Proof of Theorem ccat2s1fvw
Step | Hyp | Ref
| Expression |
1 | | simpl1 1057 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → 𝑊 ∈ Word 𝑉) |
2 | | simprl 790 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → 𝑋 ∈ 𝑉) |
3 | | simpr 476 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 𝑌 ∈ 𝑉) |
4 | 3 | adantl 481 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → 𝑌 ∈ 𝑉) |
5 | | ccatw2s1ass 13259 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) = (𝑊 ++ (〈“𝑋”〉 ++
〈“𝑌”〉))) |
6 | 1, 2, 4, 5 | syl3anc 1318 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) = (𝑊 ++ (〈“𝑋”〉 ++
〈“𝑌”〉))) |
7 | 6 | fveq1d 6105 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝐼) = ((𝑊 ++ (〈“𝑋”〉 ++ 〈“𝑌”〉))‘𝐼)) |
8 | | ccat2s1cl 13250 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (〈“𝑋”〉 ++ 〈“𝑌”〉) ∈ Word 𝑉) |
9 | 8 | adantl 481 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (〈“𝑋”〉 ++ 〈“𝑌”〉) ∈ Word 𝑉) |
10 | | simp2 1055 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) → 𝐼 ∈
ℕ0) |
11 | | lencl 13179 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
12 | 11 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) → (#‘𝑊) ∈
ℕ0) |
13 | | nn0ge0 11195 |
. . . . . . . . . 10
⊢ (𝐼 ∈ ℕ0
→ 0 ≤ 𝐼) |
14 | 13 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0) → 0 ≤
𝐼) |
15 | | 0red 9920 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0) → 0 ∈
ℝ) |
16 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0) → 𝐼 ∈
ℕ0) |
17 | 16 | nn0red 11229 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0) → 𝐼 ∈
ℝ) |
18 | 11 | nn0red 11229 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈ ℝ) |
19 | 18 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0) →
(#‘𝑊) ∈
ℝ) |
20 | | lelttr 10007 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 𝐼
∈ ℝ ∧ (#‘𝑊) ∈ ℝ) → ((0 ≤ 𝐼 ∧ 𝐼 < (#‘𝑊)) → 0 < (#‘𝑊))) |
21 | 15, 17, 19, 20 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0) → ((0 ≤
𝐼 ∧ 𝐼 < (#‘𝑊)) → 0 < (#‘𝑊))) |
22 | 14, 21 | mpand 707 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0) → (𝐼 < (#‘𝑊) → 0 < (#‘𝑊))) |
23 | 22 | 3impia 1253 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) → 0 < (#‘𝑊)) |
24 | | elnnnn0b 11214 |
. . . . . . 7
⊢
((#‘𝑊) ∈
ℕ ↔ ((#‘𝑊)
∈ ℕ0 ∧ 0 < (#‘𝑊))) |
25 | 12, 23, 24 | sylanbrc 695 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) → (#‘𝑊) ∈ ℕ) |
26 | | simp3 1056 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) → 𝐼 < (#‘𝑊)) |
27 | 10, 25, 26 | 3jca 1235 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) → (𝐼 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ 𝐼 < (#‘𝑊))) |
28 | 27 | adantr 480 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝐼 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ 𝐼 < (#‘𝑊))) |
29 | | elfzo0 12376 |
. . . 4
⊢ (𝐼 ∈ (0..^(#‘𝑊)) ↔ (𝐼 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ 𝐼 < (#‘𝑊))) |
30 | 28, 29 | sylibr 223 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → 𝐼 ∈ (0..^(#‘𝑊))) |
31 | | ccatval1 13214 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ (〈“𝑋”〉 ++ 〈“𝑌”〉) ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 ++ (〈“𝑋”〉 ++ 〈“𝑌”〉))‘𝐼) = (𝑊‘𝐼)) |
32 | 1, 9, 30, 31 | syl3anc 1318 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝑊 ++ (〈“𝑋”〉 ++ 〈“𝑌”〉))‘𝐼) = (𝑊‘𝐼)) |
33 | 7, 32 | eqtrd 2644 |
1
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝐼) = (𝑊‘𝐼)) |