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 syl5eq ( 𝑁 ∈ ( ℤ ‘ 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 ) ) = 𝑋 ) )