Proof of Theorem numclwwlk1lem2foalem
Step | Hyp | Ref
| Expression |
1 | | simpl 485 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) → 𝑊 ∈ Word 𝑉) |
2 | | s1cl 13950 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → 〈“𝑋”〉 ∈ Word 𝑉) |
3 | | s1cl 13950 |
. . . . . . . 8
⊢ (𝑌 ∈ 𝑉 → 〈“𝑌”〉 ∈ Word 𝑉) |
4 | 1, 2, 3 | 3anim123i 1147 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑊 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉 ∧ 〈“𝑌”〉 ∈ Word 𝑉)) |
5 | 4 | 3expb 1116 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑊 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉 ∧ 〈“𝑌”〉 ∈ Word 𝑉)) |
6 | | ccatass 13936 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉 ∧ 〈“𝑌”〉 ∈ Word 𝑉) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) = (𝑊 ++ (〈“𝑋”〉 ++
〈“𝑌”〉))) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) = (𝑊 ++ (〈“𝑋”〉 ++
〈“𝑌”〉))) |
8 | 7 | oveq1d 7165 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) prefix (𝑁 − 2)) = ((𝑊 ++ (〈“𝑋”〉 ++
〈“𝑌”〉)) prefix (𝑁 − 2))) |
9 | 1 | adantr 483 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → 𝑊 ∈ Word 𝑉) |
10 | | ccat2s1cl 13966 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (〈“𝑋”〉 ++ 〈“𝑌”〉) ∈ Word 𝑉) |
11 | 10 | adantl 484 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (〈“𝑋”〉 ++ 〈“𝑌”〉) ∈ Word 𝑉) |
12 | | simpr 487 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) → (♯‘𝑊) = (𝑁 − 2)) |
13 | 12 | eqcomd 2827 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) → (𝑁 − 2) = (♯‘𝑊)) |
14 | 13 | adantr 483 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑁 − 2) = (♯‘𝑊)) |
15 | | pfxccatid 14097 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ (〈“𝑋”〉 ++ 〈“𝑌”〉) ∈ Word 𝑉 ∧ (𝑁 − 2) = (♯‘𝑊)) → ((𝑊 ++ (〈“𝑋”〉 ++ 〈“𝑌”〉)) prefix (𝑁 − 2)) = 𝑊) |
16 | 9, 11, 14, 15 | syl3anc 1367 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝑊 ++ (〈“𝑋”〉 ++ 〈“𝑌”〉)) prefix (𝑁 − 2)) = 𝑊) |
17 | 8, 16 | eqtrd 2856 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) prefix (𝑁 − 2)) = 𝑊) |
18 | 17 | 3adant3 1128 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ++
〈“𝑋”〉) ++ 〈“𝑌”〉) prefix (𝑁 − 2)) = 𝑊) |
19 | | 1e2m1 11758 |
. . . . . . 7
⊢ 1 = (2
− 1) |
20 | 19 | oveq2i 7161 |
. . . . . 6
⊢ (𝑁 − 1) = (𝑁 − (2 − 1)) |
21 | | eluzelcn 12249 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℂ) |
22 | | 2cnd 11709 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ ℂ) |
23 | | 1cnd 10630 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘3) → 1 ∈ ℂ) |
24 | 21, 22, 23 | subsubd 11019 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − (2 − 1)) = ((𝑁 − 2) +
1)) |
25 | 20, 24 | syl5eq 2868 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 1) = ((𝑁 − 2) + 1)) |
26 | 25 | 3ad2ant3 1131 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 1) =
((𝑁 − 2) +
1)) |
27 | 26 | fveq2d 6668 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ++
〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) = (((𝑊 ++ 〈“𝑋”〉) ++
〈“𝑌”〉)‘((𝑁 − 2) + 1))) |
28 | | ccatw2s1p2 13991 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘((𝑁 − 2) + 1)) = 𝑌) |
29 | 28 | 3adant3 1128 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ++
〈“𝑋”〉) ++ 〈“𝑌”〉)‘((𝑁 − 2) + 1)) = 𝑌) |
30 | 27, 29 | eqtrd 2856 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ++
〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) = 𝑌) |
31 | | simpl 485 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → 𝑋 ∈ 𝑉) |
32 | | ccatw2s1p1 13989 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2) ∧ 𝑋 ∈ 𝑉) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋) |
33 | 1, 12, 31, 32 | syl2an3an 1418 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋) |
34 | 33 | 3adant3 1128 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ++
〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋) |
35 | 18, 30, 34 | 3jca 1124 |
1
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((((𝑊 ++
〈“𝑋”〉) ++ 〈“𝑌”〉) prefix (𝑁 − 2)) = 𝑊 ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 1)) = 𝑌 ∧ (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑁 − 2)) = 𝑋)) |