Proof of Theorem numclwlk1lem2foalem
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | simpl 473 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) → 𝑊 ∈ Word 𝑉) |
| 2 | | s1cl 13382 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → ⟨“𝑋”⟩ ∈ Word 𝑉) |
| 3 | | s1cl 13382 |
. . . . . . . 8
⊢ (𝑌 ∈ 𝑉 → ⟨“𝑌”⟩ ∈ Word 𝑉) |
| 4 | 1, 2, 3 | 3anim123i 1247 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑊 ∈ Word 𝑉 ∧ ⟨“𝑋”⟩ ∈ Word 𝑉 ∧ ⟨“𝑌”⟩ ∈ Word 𝑉)) |
| 5 | 4 | 3expb 1266 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑊 ∈ Word 𝑉 ∧ ⟨“𝑋”⟩ ∈ Word 𝑉 ∧ ⟨“𝑌”⟩ ∈ Word 𝑉)) |
| 6 | | ccatass 13371 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑋”⟩ ∈ Word 𝑉 ∧ ⟨“𝑌”⟩ ∈ Word 𝑉) → ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) = (𝑊 ++ (⟨“𝑋”⟩ ++
⟨“𝑌”⟩))) |
| 7 | 5, 6 | syl 17 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) = (𝑊 ++ (⟨“𝑋”⟩ ++
⟨“𝑌”⟩))) |
| 8 | 7 | oveq1d 6665 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) substr ⟨0,
(𝑁 − 2)⟩) =
((𝑊 ++ (⟨“𝑋”⟩ ++
⟨“𝑌”⟩)) substr ⟨0, (𝑁 −
2)⟩)) |
| 9 | 1 | adantr 481 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → 𝑊 ∈ Word 𝑉) |
| 10 | | ccat2s1cl 13397 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (⟨“𝑋”⟩ ++ ⟨“𝑌”⟩) ∈ Word 𝑉) |
| 11 | 10 | adantl 482 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (⟨“𝑋”⟩ ++ ⟨“𝑌”⟩) ∈ Word 𝑉) |
| 12 | | simpr 477 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) → (#‘𝑊) = (𝑁 − 2)) |
| 13 | 12 | eqcomd 2628 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) → (𝑁 − 2) = (#‘𝑊)) |
| 14 | 13 | adantr 481 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑁 − 2) = (#‘𝑊)) |
| 15 | | swrdccatid 13497 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ (⟨“𝑋”⟩ ++ ⟨“𝑌”⟩) ∈ Word 𝑉 ∧ (𝑁 − 2) = (#‘𝑊)) → ((𝑊 ++ (⟨“𝑋”⟩ ++ ⟨“𝑌”⟩)) substr ⟨0,
(𝑁 − 2)⟩) =
𝑊) |
| 16 | 9, 11, 14, 15 | syl3anc 1326 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ((𝑊 ++ (⟨“𝑋”⟩ ++ ⟨“𝑌”⟩)) substr ⟨0,
(𝑁 − 2)⟩) =
𝑊) |
| 17 | 8, 16 | eqtrd 2656 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) substr ⟨0,
(𝑁 − 2)⟩) =
𝑊) |
| 18 | 17 | 3adant3 1081 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ++
⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) substr ⟨0,
(𝑁 − 2)⟩) =
𝑊) |
| 19 | | 1e2m1 11136 |
. . . . . . 7
⊢ 1 = (2
− 1) |
| 20 | 19 | oveq2i 6661 |
. . . . . 6
⊢ (𝑁 − 1) = (𝑁 − (2 − 1)) |
| 21 | | eluzelcn 11699 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℂ) |
| 22 | | 2cnd 11093 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ ℂ) |
| 23 | | 1cnd 10056 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘3) → 1 ∈ ℂ) |
| 24 | 21, 22, 23 | subsubd 10420 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − (2 − 1)) = ((𝑁 − 2) +
1)) |
| 25 | 20, 24 | syl5eq 2668 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 1) = ((𝑁 − 2) + 1)) |
| 26 | 25 | 3ad2ant3 1084 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 1) =
((𝑁 − 2) +
1)) |
| 27 | 26 | fveq2d 6195 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ++
⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑁 − 1)) = (((𝑊 ++ ⟨“𝑋”⟩) ++
⟨“𝑌”⟩)‘((𝑁 − 2) + 1))) |
| 28 | | ccatw2s1p2 13414 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((𝑁 − 2) + 1)) = 𝑌) |
| 29 | 28 | 3adant3 1081 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ++
⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘((𝑁 − 2) + 1)) = 𝑌) |
| 30 | 27, 29 | eqtrd 2656 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ++
⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑁 − 1)) = 𝑌) |
| 31 | | ccatw2s1p1 13413 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑁 − 2)) = 𝑋) |
| 32 | 31 | 3adant3 1081 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑊 ++
⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑁 − 2)) = 𝑋) |
| 33 | 18, 30, 32 | 3jca 1242 |
1
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((((𝑊 ++
⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) substr ⟨0,
(𝑁 − 2)⟩) =
𝑊 ∧ (((𝑊 ++ ⟨“𝑋”⟩) ++
⟨“𝑌”⟩)‘(𝑁 − 1)) = 𝑌 ∧ (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑁 − 2)) = 𝑋)) |
