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 
|- ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) = W /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 1 ) ) = Y /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 2 ) ) = X ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) -> W e. Word V )
2 s1cl 
 |-  ( X e. V -> <" X "> e. Word V )
3 s1cl 
 |-  ( Y e. V -> <" Y "> e. Word V )
4 1 2 3 3anim123i 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ X e. V /\ Y e. V ) -> ( W e. Word V /\ <" X "> e. Word V /\ <" Y "> e. Word V ) )
5 4 3expb 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) ) -> ( W e. Word V /\ <" X "> e. Word V /\ <" Y "> e. Word V ) )
6 ccatass 
 |-  ( ( W e. Word V /\ <" X "> e. Word V /\ <" Y "> e. Word V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ ( <" X "> ++ <" Y "> ) ) )
7 5 6 syl 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ ( <" X "> ++ <" Y "> ) ) )
8 7 oveq1d 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) = ( ( W ++ ( <" X "> ++ <" Y "> ) ) prefix ( N - 2 ) ) )
9 1 adantr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) ) -> W e. Word V )
10 ccat2s1cl 
 |-  ( ( X e. V /\ Y e. V ) -> ( <" X "> ++ <" Y "> ) e. Word V )
11 10 adantl 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) ) -> ( <" X "> ++ <" Y "> ) e. Word V )
12 simpr 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) -> ( # ` W ) = ( N - 2 ) )
13 12 eqcomd 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) -> ( N - 2 ) = ( # ` W ) )
14 13 adantr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) ) -> ( N - 2 ) = ( # ` W ) )
15 pfxccatid 
 |-  ( ( W e. Word V /\ ( <" X "> ++ <" Y "> ) e. Word V /\ ( N - 2 ) = ( # ` W ) ) -> ( ( W ++ ( <" X "> ++ <" Y "> ) ) prefix ( N - 2 ) ) = W )
16 9 11 14 15 syl3anc 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( W ++ ( <" X "> ++ <" Y "> ) ) prefix ( N - 2 ) ) = W )
17 8 16 eqtrd 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) = W )
18 17 3adant3 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) = W )
19 1e2m1 
 |-  1 = ( 2 - 1 )
20 19 oveq2i 
 |-  ( N - 1 ) = ( N - ( 2 - 1 ) )
21 eluzelcn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. CC )
22 2cnd 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 e. CC )
23 1cnd 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. CC )
24 21 22 23 subsubd 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - ( 2 - 1 ) ) = ( ( N - 2 ) + 1 ) )
25 20 24 syl5eq 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 1 ) = ( ( N - 2 ) + 1 ) )
26 25 3ad2ant3 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) -> ( N - 1 ) = ( ( N - 2 ) + 1 ) )
27 26 fveq2d 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 1 ) ) = ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( N - 2 ) + 1 ) ) )
28 ccatw2s1p2 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( N - 2 ) + 1 ) ) = Y )
29 28 3adant3 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( ( N - 2 ) + 1 ) ) = Y )
30 27 29 eqtrd 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 1 ) ) = Y )
31 simpl 
 |-  ( ( X e. V /\ Y e. V ) -> X e. V )
32 ccatw2s1p1 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) /\ X e. V ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 2 ) ) = X )
33 1 12 31 32 syl2an3an 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 2 ) ) = X )
34 33 3adant3 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 2 ) ) = X )
35 18 30 34 3jca 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = ( N - 2 ) ) /\ ( X e. V /\ Y e. V ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) prefix ( N - 2 ) ) = W /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 1 ) ) = Y /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( N - 2 ) ) = X ) )