Metamath Proof Explorer

Theorem numclwwlk1lem2foalem

Description: Lemma for numclwwlk1lem2foa . (Contributed by AV, 29-May-2021) (Revised by AV, 1-Nov-2022)

Ref Expression
Assertion numclwwlk1lem2foalem ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) = 𝑊 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 1 ) ) = 𝑌 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → 𝑊 ∈ Word 𝑉 )
2 s1cl ⊢ ( 𝑋 ∈ 𝑉 → ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 )
3 s1cl ⊢ ( 𝑌 ∈ 𝑉 → ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 )
4 1 2 3 3anim123i ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 ) )
5 4 3expb ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 ) )
6 ccatass ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑉 ∧ ⟨“ 𝑌 ”⟩ ∈ Word 𝑉 ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) )
7 5 6 syl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) = ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) )
8 7 oveq1d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) = ( ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) prefix ( 𝑁 − 2 ) ) )
9 1 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → 𝑊 ∈ Word 𝑉 )
10 ccat2s1cl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 )
11 10 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 )
12 simpr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) )
13 12 eqcomd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( 𝑁 − 2 ) = ( ♯ ‘ 𝑊 ) )
14 13 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑁 − 2 ) = ( ♯ ‘ 𝑊 ) )
15 pfxccatid ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ∈ Word 𝑉 ∧ ( 𝑁 − 2 ) = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) prefix ( 𝑁 − 2 ) ) = 𝑊 )
16 9 11 14 15 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝑊 ++ ( ⟨“ 𝑋 ”⟩ ++ ⟨“ 𝑌 ”⟩ ) ) prefix ( 𝑁 − 2 ) ) = 𝑊 )
17 8 16 eqtrd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) = 𝑊 )
18 17 3adant3 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) = 𝑊 )
19 1e2m1 ⊢ 1 = ( 2 − 1 )
20 19 oveq2i ⊢ ( 𝑁 − 1 ) = ( 𝑁 − ( 2 − 1 ) )
21 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℂ )
22 2cnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ∈ ℂ )
23 1cnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ℂ )
24 21 22 23 subsubd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − ( 2 − 1 ) ) = ( ( 𝑁 − 2 ) + 1 ) )
25 20 24 eqtrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 1 ) = ( ( 𝑁 − 2 ) + 1 ) )
26 25 3ad2ant3 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑁 − 1 ) = ( ( 𝑁 − 2 ) + 1 ) )
27 26 fveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 1 ) ) = ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) )
28 ccatw2s1p2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) = 𝑌 )
29 28 3adant3 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( ( 𝑁 − 2 ) + 1 ) ) = 𝑌 )
30 27 29 eqtrd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 1 ) ) = 𝑌 )
31 simpl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
32 ccatw2s1p1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = 𝑋 )
33 1 12 31 32 syl2an3an ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = 𝑋 )
34 33 3adant3 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = 𝑋 )
35 18 30 34 3jca ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) prefix ( 𝑁 − 2 ) ) = 𝑊 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 1 ) ) = 𝑌 ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )