Metamath Proof Explorer

Theorem 2clwwlk2clwwlklem

Description: Lemma for 2clwwlk2clwwlk . (Contributed by AV, 27-Apr-2022)

Ref Expression
Assertion 2clwwlk2clwwlklem 
|- ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> ( W substr <. ( N - 2 ) , N >. ) e. ( X ( ClWWalksNOn ` G ) 2 ) )

Proof

Step Hyp Ref Expression
1 isclwwlknon 
 |-  ( W e. ( X ( ClWWalksNOn ` G ) N ) <-> ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 2 clwwlknbp 
 |-  ( W e. ( N ClWWalksN G ) -> ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) )
4 simpll 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ N e. ( ZZ>= ` 3 ) ) -> W e. Word ( Vtx ` G ) )
5 uzuzle23 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
6 eluzfz2 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. ( 2 ... N ) )
7 5 6 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( 2 ... N ) )
8 7 adantl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ N e. ( ZZ>= ` 3 ) ) -> N e. ( 2 ... N ) )
9 oveq2 
 |-  ( ( # ` W ) = N -> ( 2 ... ( # ` W ) ) = ( 2 ... N ) )
10 9 eleq2d 
 |-  ( ( # ` W ) = N -> ( N e. ( 2 ... ( # ` W ) ) <-> N e. ( 2 ... N ) ) )
11 10 ad2antlr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ N e. ( ZZ>= ` 3 ) ) -> ( N e. ( 2 ... ( # ` W ) ) <-> N e. ( 2 ... N ) ) )
12 8 11 mpbird 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ N e. ( ZZ>= ` 3 ) ) -> N e. ( 2 ... ( # ` W ) ) )
13 4 12 jca 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. Word ( Vtx ` G ) /\ N e. ( 2 ... ( # ` W ) ) ) )
14 13 ex 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) -> ( N e. ( ZZ>= ` 3 ) -> ( W e. Word ( Vtx ` G ) /\ N e. ( 2 ... ( # ` W ) ) ) ) )
15 3 14 syl 
 |-  ( W e. ( N ClWWalksN G ) -> ( N e. ( ZZ>= ` 3 ) -> ( W e. Word ( Vtx ` G ) /\ N e. ( 2 ... ( # ` W ) ) ) ) )
16 15 adantr 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) -> ( N e. ( ZZ>= ` 3 ) -> ( W e. Word ( Vtx ` G ) /\ N e. ( 2 ... ( # ` W ) ) ) ) )
17 1 16 sylbi 
 |-  ( W e. ( X ( ClWWalksNOn ` G ) N ) -> ( N e. ( ZZ>= ` 3 ) -> ( W e. Word ( Vtx ` G ) /\ N e. ( 2 ... ( # ` W ) ) ) ) )
18 17 impcom 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) ) -> ( W e. Word ( Vtx ` G ) /\ N e. ( 2 ... ( # ` W ) ) ) )
19 swrds2m 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 2 ... ( # ` W ) ) ) -> ( W substr <. ( N - 2 ) , N >. ) = <" ( W ` ( N - 2 ) ) ( W ` ( N - 1 ) ) "> )
20 18 19 syl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) ) -> ( W substr <. ( N - 2 ) , N >. ) = <" ( W ` ( N - 2 ) ) ( W ` ( N - 1 ) ) "> )
21 20 3adant3 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> ( W substr <. ( N - 2 ) , N >. ) = <" ( W ` ( N - 2 ) ) ( W ` ( N - 1 ) ) "> )
22 simp3 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> ( W ` ( N - 2 ) ) = ( W ` 0 ) )
23 eqidd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> ( W ` ( N - 1 ) ) = ( W ` ( N - 1 ) ) )
24 22 23 s2eqd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> <" ( W ` ( N - 2 ) ) ( W ` ( N - 1 ) ) "> = <" ( W ` 0 ) ( W ` ( N - 1 ) ) "> )
25 simpr 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) -> ( W ` 0 ) = X )
26 eqidd 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) -> ( W ` ( N - 1 ) ) = ( W ` ( N - 1 ) ) )
27 25 26 s2eqd 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) -> <" ( W ` 0 ) ( W ` ( N - 1 ) ) "> = <" X ( W ` ( N - 1 ) ) "> )
28 1 27 sylbi 
 |-  ( W e. ( X ( ClWWalksNOn ` G ) N ) -> <" ( W ` 0 ) ( W ` ( N - 1 ) ) "> = <" X ( W ` ( N - 1 ) ) "> )
29 28 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> <" ( W ` 0 ) ( W ` ( N - 1 ) ) "> = <" X ( W ` ( N - 1 ) ) "> )
30 21 24 29 3eqtrd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> ( W substr <. ( N - 2 ) , N >. ) = <" X ( W ` ( N - 1 ) ) "> )
31 clwwlknonmpo 
 |-  ( ClWWalksNOn ` G ) = ( v e. ( Vtx ` G ) , n e. NN0 |-> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } )
32 31 elmpocl1 
 |-  ( W e. ( X ( ClWWalksNOn ` G ) N ) -> X e. ( Vtx ` G ) )
33 32 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> X e. ( Vtx ` G ) )
34 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
35 fzo0end 
 |-  ( N e. NN -> ( N - 1 ) e. ( 0 ..^ N ) )
36 34 35 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 1 ) e. ( 0 ..^ N ) )
37 36 adantl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ N e. ( ZZ>= ` 3 ) ) -> ( N - 1 ) e. ( 0 ..^ N ) )
38 oveq2 
 |-  ( ( # ` W ) = N -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ N ) )
39 38 ad2antlr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ N e. ( ZZ>= ` 3 ) ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ N ) )
40 39 eleq2d 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( N - 1 ) e. ( 0 ..^ ( # ` W ) ) <-> ( N - 1 ) e. ( 0 ..^ N ) ) )
41 37 40 mpbird 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ N e. ( ZZ>= ` 3 ) ) -> ( N - 1 ) e. ( 0 ..^ ( # ` W ) ) )
42 wrdsymbcl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( N - 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` ( N - 1 ) ) e. ( Vtx ` G ) )
43 4 41 42 syl2anc 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ N e. ( ZZ>= ` 3 ) ) -> ( W ` ( N - 1 ) ) e. ( Vtx ` G ) )
44 43 ex 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) -> ( N e. ( ZZ>= ` 3 ) -> ( W ` ( N - 1 ) ) e. ( Vtx ` G ) ) )
45 3 44 syl 
 |-  ( W e. ( N ClWWalksN G ) -> ( N e. ( ZZ>= ` 3 ) -> ( W ` ( N - 1 ) ) e. ( Vtx ` G ) ) )
46 45 adantr 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) -> ( N e. ( ZZ>= ` 3 ) -> ( W ` ( N - 1 ) ) e. ( Vtx ` G ) ) )
47 1 46 sylbi 
 |-  ( W e. ( X ( ClWWalksNOn ` G ) N ) -> ( N e. ( ZZ>= ` 3 ) -> ( W ` ( N - 1 ) ) e. ( Vtx ` G ) ) )
48 47 impcom 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) ) -> ( W ` ( N - 1 ) ) e. ( Vtx ` G ) )
49 48 3adant3 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> ( W ` ( N - 1 ) ) e. ( Vtx ` G ) )
50 preq1 
 |-  ( ( W ` 0 ) = X -> { ( W ` 0 ) , ( W ` ( N - 1 ) ) } = { X , ( W ` ( N - 1 ) ) } )
51 50 adantl 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) -> { ( W ` 0 ) , ( W ` ( N - 1 ) ) } = { X , ( W ` ( N - 1 ) ) } )
52 51 eqcomd 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) -> { X , ( W ` ( N - 1 ) ) } = { ( W ` 0 ) , ( W ` ( N - 1 ) ) } )
53 52 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> { X , ( W ` ( N - 1 ) ) } = { ( W ` 0 ) , ( W ` ( N - 1 ) ) } )
54 prcom 
 |-  { ( W ` 0 ) , ( W ` ( N - 1 ) ) } = { ( W ` ( N - 1 ) ) , ( W ` 0 ) }
55 53 54 eqtrdi 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> { X , ( W ` ( N - 1 ) ) } = { ( W ` ( N - 1 ) ) , ( W ` 0 ) } )
56 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
57 2 56 clwwlknp 
 |-  ( W e. ( N ClWWalksN G ) -> ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
58 57 adantr 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) -> ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
59 58 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
60 lsw 
 |-  ( W e. Word ( Vtx ` G ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
61 fvoveq1 
 |-  ( ( # ` W ) = N -> ( W ` ( ( # ` W ) - 1 ) ) = ( W ` ( N - 1 ) ) )
62 60 61 sylan9eq 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) -> ( lastS ` W ) = ( W ` ( N - 1 ) ) )
63 62 adantr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ ( N e. ( ZZ>= ` 3 ) /\ ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) ) -> ( lastS ` W ) = ( W ` ( N - 1 ) ) )
64 63 preq1d 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ ( N e. ( ZZ>= ` 3 ) /\ ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) ) -> { ( lastS ` W ) , ( W ` 0 ) } = { ( W ` ( N - 1 ) ) , ( W ` 0 ) } )
65 64 eleq1d 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ ( N e. ( ZZ>= ` 3 ) /\ ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) <-> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
66 65 biimpd 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ ( N e. ( ZZ>= ` 3 ) /\ ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
67 66 ex 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) -> ( ( N e. ( ZZ>= ` 3 ) /\ ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
68 67 com23 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> ( ( N e. ( ZZ>= ` 3 ) /\ ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) )
69 68 a1d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> ( ( N e. ( ZZ>= ` 3 ) /\ ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) ) ) ) )
70 69 3imp 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) -> ( ( N e. ( ZZ>= ` 3 ) /\ ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
71 59 70 mpcom 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> { ( W ` ( N - 1 ) ) , ( W ` 0 ) } e. ( Edg ` G ) )
72 55 71 eqeltrd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> { X , ( W ` ( N - 1 ) ) } e. ( Edg ` G ) )
73 1 72 syl3an2b 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> { X , ( W ` ( N - 1 ) ) } e. ( Edg ` G ) )
74 eqid 
 |-  ( ClWWalksNOn ` G ) = ( ClWWalksNOn ` G )
75 74 2 56 s2elclwwlknon2 
 |-  ( ( X e. ( Vtx ` G ) /\ ( W ` ( N - 1 ) ) e. ( Vtx ` G ) /\ { X , ( W ` ( N - 1 ) ) } e. ( Edg ` G ) ) -> <" X ( W ` ( N - 1 ) ) "> e. ( X ( ClWWalksNOn ` G ) 2 ) )
76 33 49 73 75 syl3anc 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> <" X ( W ` ( N - 1 ) ) "> e. ( X ( ClWWalksNOn ` G ) 2 ) )
77 30 76 eqeltrd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> ( W substr <. ( N - 2 ) , N >. ) e. ( X ( ClWWalksNOn ` G ) 2 ) )