Metamath Proof Explorer

Theorem 2clwwlk2clwwlk

Description: An element of the value of operation C , i.e., a word being a double loop of length N on vertex X , is composed of two closed walks. (Contributed by AV, 28-Apr-2022) (Proof shortened by AV, 3-Nov-2022)

Ref Expression
Hypothesis 2clwwlk.c 
|- C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
Assertion 2clwwlk2clwwlk 
|- ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. ( X C N ) <-> E. a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) E. b e. ( X ( ClWWalksNOn ` G ) 2 ) W = ( a ++ b ) ) )

Proof

Step Hyp Ref Expression
1 2clwwlk.c 
 |-  C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
2 uzuzle23 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
3 1 2clwwlkel 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( W e. ( X C N ) <-> ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) )
4 2 3 sylan2 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. ( X C N ) <-> ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) )
5 simpr 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> N e. ( ZZ>= ` 3 ) )
6 5 anim1i 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) -> ( N e. ( ZZ>= ` 3 ) /\ ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) )
7 3anass 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) <-> ( N e. ( ZZ>= ` 3 ) /\ ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) )
8 6 7 sylibr 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) -> ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) )
9 clwwnonrepclwwnon 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) -> ( W prefix ( N - 2 ) ) e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) )
10 8 9 syl 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) -> ( W prefix ( N - 2 ) ) e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) )
11 5 adantr 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) -> N e. ( ZZ>= ` 3 ) )
12 simprl 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) -> W e. ( X ( ClWWalksNOn ` G ) N ) )
13 simprr 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) -> ( W ` ( N - 2 ) ) = X )
14 isclwwlknon 
 |-  ( W e. ( X ( ClWWalksNOn ` G ) N ) <-> ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) )
15 simpr 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) -> ( W ` 0 ) = X )
16 15 eqcomd 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) -> X = ( W ` 0 ) )
17 14 16 sylbi 
 |-  ( W e. ( X ( ClWWalksNOn ` G ) N ) -> X = ( W ` 0 ) )
18 17 ad2antrl 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) -> X = ( W ` 0 ) )
19 13 18 eqtrd 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) -> ( W ` ( N - 2 ) ) = ( W ` 0 ) )
20 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 ) )
21 11 12 19 20 syl3anc 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) -> ( W substr <. ( N - 2 ) , N >. ) e. ( X ( ClWWalksNOn ` G ) 2 ) )
22 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
23 22 clwwlknbp 
 |-  ( W e. ( N ClWWalksN G ) -> ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) )
24 opeq2 
 |-  ( N = ( # ` W ) -> <. ( N - 2 ) , N >. = <. ( N - 2 ) , ( # ` W ) >. )
25 24 oveq2d 
 |-  ( N = ( # ` W ) -> ( W substr <. ( N - 2 ) , N >. ) = ( W substr <. ( N - 2 ) , ( # ` W ) >. ) )
26 25 oveq2d 
 |-  ( N = ( # ` W ) -> ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , N >. ) ) = ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , ( # ` W ) >. ) ) )
27 26 eqcoms 
 |-  ( ( # ` W ) = N -> ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , N >. ) ) = ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , ( # ` W ) >. ) ) )
28 27 ad2antlr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , N >. ) ) = ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , ( # ` W ) >. ) ) )
29 simpl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) -> W e. Word ( Vtx ` G ) )
30 fz1ssfz0 
 |-  ( 1 ... N ) C_ ( 0 ... N )
31 ige3m2fz 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. ( 1 ... N ) )
32 30 31 sseldi 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. ( 0 ... N ) )
33 32 adantl 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( N - 2 ) e. ( 0 ... N ) )
34 33 adantl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( N - 2 ) e. ( 0 ... N ) )
35 oveq2 
 |-  ( ( # ` W ) = N -> ( 0 ... ( # ` W ) ) = ( 0 ... N ) )
36 35 eleq2d 
 |-  ( ( # ` W ) = N -> ( ( N - 2 ) e. ( 0 ... ( # ` W ) ) <-> ( N - 2 ) e. ( 0 ... N ) ) )
37 36 ad2antlr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( N - 2 ) e. ( 0 ... ( # ` W ) ) <-> ( N - 2 ) e. ( 0 ... N ) ) )
38 34 37 mpbird 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( N - 2 ) e. ( 0 ... ( # ` W ) ) )
39 pfxcctswrd 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( N - 2 ) e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , ( # ` W ) >. ) ) = W )
40 29 38 39 syl2an2r 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , ( # ` W ) >. ) ) = W )
41 28 40 eqtrd 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , N >. ) ) = W )
42 23 41 sylan 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , N >. ) ) = W )
43 42 ex 
 |-  ( W e. ( N ClWWalksN G ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , N >. ) ) = W ) )
44 43 adantr 
 |-  ( ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , N >. ) ) = W ) )
45 14 44 sylbi 
 |-  ( W e. ( X ( ClWWalksNOn ` G ) N ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , N >. ) ) = W ) )
46 45 adantr 
 |-  ( ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , N >. ) ) = W ) )
47 46 impcom 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) -> ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , N >. ) ) = W )
48 47 eqcomd 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) -> W = ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , N >. ) ) )
49 10 21 48 3jca 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) ) -> ( ( W prefix ( N - 2 ) ) e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) /\ ( W substr <. ( N - 2 ) , N >. ) e. ( X ( ClWWalksNOn ` G ) 2 ) /\ W = ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , N >. ) ) ) )
50 49 ex 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( W e. ( X ( ClWWalksNOn ` G ) N ) /\ ( W ` ( N - 2 ) ) = X ) -> ( ( W prefix ( N - 2 ) ) e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) /\ ( W substr <. ( N - 2 ) , N >. ) e. ( X ( ClWWalksNOn ` G ) 2 ) /\ W = ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , N >. ) ) ) ) )
51 4 50 sylbid 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. ( X C N ) -> ( ( W prefix ( N - 2 ) ) e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) /\ ( W substr <. ( N - 2 ) , N >. ) e. ( X ( ClWWalksNOn ` G ) 2 ) /\ W = ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , N >. ) ) ) ) )
52 rspceov 
 |-  ( ( ( W prefix ( N - 2 ) ) e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) /\ ( W substr <. ( N - 2 ) , N >. ) e. ( X ( ClWWalksNOn ` G ) 2 ) /\ W = ( ( W prefix ( N - 2 ) ) ++ ( W substr <. ( N - 2 ) , N >. ) ) ) -> E. a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) E. b e. ( X ( ClWWalksNOn ` G ) 2 ) W = ( a ++ b ) )
53 51 52 syl6 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. ( X C N ) -> E. a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) E. b e. ( X ( ClWWalksNOn ` G ) 2 ) W = ( a ++ b ) ) )
54 eluzelcn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. CC )
55 2cnd 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 e. CC )
56 54 55 npcand 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) + 2 ) = N )
57 56 adantl 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( N - 2 ) + 2 ) = N )
58 57 oveq2d 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( X ( ClWWalksNOn ` G ) ( ( N - 2 ) + 2 ) ) = ( X ( ClWWalksNOn ` G ) N ) )
59 58 eleq2d 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ b ) e. ( X ( ClWWalksNOn ` G ) ( ( N - 2 ) + 2 ) ) <-> ( a ++ b ) e. ( X ( ClWWalksNOn ` G ) N ) ) )
60 59 biimpd 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ b ) e. ( X ( ClWWalksNOn ` G ) ( ( N - 2 ) + 2 ) ) -> ( a ++ b ) e. ( X ( ClWWalksNOn ` G ) N ) ) )
61 clwwlknonccat 
 |-  ( ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) /\ b e. ( X ( ClWWalksNOn ` G ) 2 ) ) -> ( a ++ b ) e. ( X ( ClWWalksNOn ` G ) ( ( N - 2 ) + 2 ) ) )
62 60 61 impel 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) /\ b e. ( X ( ClWWalksNOn ` G ) 2 ) ) ) -> ( a ++ b ) e. ( X ( ClWWalksNOn ` G ) N ) )
63 isclwwlknon 
 |-  ( b e. ( X ( ClWWalksNOn ` G ) 2 ) <-> ( b e. ( 2 ClWWalksN G ) /\ ( b ` 0 ) = X ) )
64 clwwlkn2 
 |-  ( b e. ( 2 ClWWalksN G ) <-> ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) /\ { ( b ` 0 ) , ( b ` 1 ) } e. ( Edg ` G ) ) )
65 isclwwlknon 
 |-  ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) <-> ( a e. ( ( N - 2 ) ClWWalksN G ) /\ ( a ` 0 ) = X ) )
66 22 clwwlknbp 
 |-  ( a e. ( ( N - 2 ) ClWWalksN G ) -> ( a e. Word ( Vtx ` G ) /\ ( # ` a ) = ( N - 2 ) ) )
67 simpl 
 |-  ( ( a e. Word ( Vtx ` G ) /\ ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) ) -> a e. Word ( Vtx ` G ) )
68 simprr 
 |-  ( ( a e. Word ( Vtx ` G ) /\ ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) ) -> b e. Word ( Vtx ` G ) )
69 2nn 
 |-  2 e. NN
70 lbfzo0 
 |-  ( 0 e. ( 0 ..^ 2 ) <-> 2 e. NN )
71 69 70 mpbir 
 |-  0 e. ( 0 ..^ 2 )
72 oveq2 
 |-  ( ( # ` b ) = 2 -> ( 0 ..^ ( # ` b ) ) = ( 0 ..^ 2 ) )
73 71 72 eleqtrrid 
 |-  ( ( # ` b ) = 2 -> 0 e. ( 0 ..^ ( # ` b ) ) )
74 73 ad2antrl 
 |-  ( ( a e. Word ( Vtx ` G ) /\ ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) ) -> 0 e. ( 0 ..^ ( # ` b ) ) )
75 67 68 74 3jca 
 |-  ( ( a e. Word ( Vtx ` G ) /\ ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) ) -> ( a e. Word ( Vtx ` G ) /\ b e. Word ( Vtx ` G ) /\ 0 e. ( 0 ..^ ( # ` b ) ) ) )
76 75 adantr 
 |-  ( ( ( a e. Word ( Vtx ` G ) /\ ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) ) /\ ( ( b ` 0 ) = X /\ ( # ` a ) = ( N - 2 ) ) ) -> ( a e. Word ( Vtx ` G ) /\ b e. Word ( Vtx ` G ) /\ 0 e. ( 0 ..^ ( # ` b ) ) ) )
77 76 adantr 
 |-  ( ( ( ( a e. Word ( Vtx ` G ) /\ ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) ) /\ ( ( b ` 0 ) = X /\ ( # ` a ) = ( N - 2 ) ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( a e. Word ( Vtx ` G ) /\ b e. Word ( Vtx ` G ) /\ 0 e. ( 0 ..^ ( # ` b ) ) ) )
78 ccatval3 
 |-  ( ( a e. Word ( Vtx ` G ) /\ b e. Word ( Vtx ` G ) /\ 0 e. ( 0 ..^ ( # ` b ) ) ) -> ( ( a ++ b ) ` ( 0 + ( # ` a ) ) ) = ( b ` 0 ) )
79 77 78 syl 
 |-  ( ( ( ( a e. Word ( Vtx ` G ) /\ ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) ) /\ ( ( b ` 0 ) = X /\ ( # ` a ) = ( N - 2 ) ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( a ++ b ) ` ( 0 + ( # ` a ) ) ) = ( b ` 0 ) )
80 simpr 
 |-  ( ( ( b ` 0 ) = X /\ ( # ` a ) = ( N - 2 ) ) -> ( # ` a ) = ( N - 2 ) )
81 80 oveq2d 
 |-  ( ( ( b ` 0 ) = X /\ ( # ` a ) = ( N - 2 ) ) -> ( 0 + ( # ` a ) ) = ( 0 + ( N - 2 ) ) )
82 81 adantl 
 |-  ( ( ( a e. Word ( Vtx ` G ) /\ ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) ) /\ ( ( b ` 0 ) = X /\ ( # ` a ) = ( N - 2 ) ) ) -> ( 0 + ( # ` a ) ) = ( 0 + ( N - 2 ) ) )
83 54 55 subcld 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. CC )
84 83 addid2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( 0 + ( N - 2 ) ) = ( N - 2 ) )
85 84 adantl 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( 0 + ( N - 2 ) ) = ( N - 2 ) )
86 82 85 sylan9eq 
 |-  ( ( ( ( a e. Word ( Vtx ` G ) /\ ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) ) /\ ( ( b ` 0 ) = X /\ ( # ` a ) = ( N - 2 ) ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( 0 + ( # ` a ) ) = ( N - 2 ) )
87 86 eqcomd 
 |-  ( ( ( ( a e. Word ( Vtx ` G ) /\ ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) ) /\ ( ( b ` 0 ) = X /\ ( # ` a ) = ( N - 2 ) ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( N - 2 ) = ( 0 + ( # ` a ) ) )
88 87 fveq2d 
 |-  ( ( ( ( a e. Word ( Vtx ` G ) /\ ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) ) /\ ( ( b ` 0 ) = X /\ ( # ` a ) = ( N - 2 ) ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( a ++ b ) ` ( N - 2 ) ) = ( ( a ++ b ) ` ( 0 + ( # ` a ) ) ) )
89 simpl 
 |-  ( ( ( b ` 0 ) = X /\ ( # ` a ) = ( N - 2 ) ) -> ( b ` 0 ) = X )
90 89 eqcomd 
 |-  ( ( ( b ` 0 ) = X /\ ( # ` a ) = ( N - 2 ) ) -> X = ( b ` 0 ) )
91 90 ad2antlr 
 |-  ( ( ( ( a e. Word ( Vtx ` G ) /\ ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) ) /\ ( ( b ` 0 ) = X /\ ( # ` a ) = ( N - 2 ) ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> X = ( b ` 0 ) )
92 79 88 91 3eqtr4d 
 |-  ( ( ( ( a e. Word ( Vtx ` G ) /\ ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) ) /\ ( ( b ` 0 ) = X /\ ( # ` a ) = ( N - 2 ) ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( a ++ b ) ` ( N - 2 ) ) = X )
93 92 exp53 
 |-  ( a e. Word ( Vtx ` G ) -> ( ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) -> ( ( b ` 0 ) = X -> ( ( # ` a ) = ( N - 2 ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ b ) ` ( N - 2 ) ) = X ) ) ) ) )
94 93 com24 
 |-  ( a e. Word ( Vtx ` G ) -> ( ( # ` a ) = ( N - 2 ) -> ( ( b ` 0 ) = X -> ( ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ b ) ` ( N - 2 ) ) = X ) ) ) ) )
95 94 imp 
 |-  ( ( a e. Word ( Vtx ` G ) /\ ( # ` a ) = ( N - 2 ) ) -> ( ( b ` 0 ) = X -> ( ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ b ) ` ( N - 2 ) ) = X ) ) ) )
96 66 95 syl 
 |-  ( a e. ( ( N - 2 ) ClWWalksN G ) -> ( ( b ` 0 ) = X -> ( ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ b ) ` ( N - 2 ) ) = X ) ) ) )
97 96 adantr 
 |-  ( ( a e. ( ( N - 2 ) ClWWalksN G ) /\ ( a ` 0 ) = X ) -> ( ( b ` 0 ) = X -> ( ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ b ) ` ( N - 2 ) ) = X ) ) ) )
98 65 97 sylbi 
 |-  ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) -> ( ( b ` 0 ) = X -> ( ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ b ) ` ( N - 2 ) ) = X ) ) ) )
99 98 com13 
 |-  ( ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) ) -> ( ( b ` 0 ) = X -> ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ b ) ` ( N - 2 ) ) = X ) ) ) )
100 99 3adant3 
 |-  ( ( ( # ` b ) = 2 /\ b e. Word ( Vtx ` G ) /\ { ( b ` 0 ) , ( b ` 1 ) } e. ( Edg ` G ) ) -> ( ( b ` 0 ) = X -> ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ b ) ` ( N - 2 ) ) = X ) ) ) )
101 64 100 sylbi 
 |-  ( b e. ( 2 ClWWalksN G ) -> ( ( b ` 0 ) = X -> ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ b ) ` ( N - 2 ) ) = X ) ) ) )
102 101 imp 
 |-  ( ( b e. ( 2 ClWWalksN G ) /\ ( b ` 0 ) = X ) -> ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ b ) ` ( N - 2 ) ) = X ) ) )
103 63 102 sylbi 
 |-  ( b e. ( X ( ClWWalksNOn ` G ) 2 ) -> ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ b ) ` ( N - 2 ) ) = X ) ) )
104 103 impcom 
 |-  ( ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) /\ b e. ( X ( ClWWalksNOn ` G ) 2 ) ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ b ) ` ( N - 2 ) ) = X ) )
105 104 impcom 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) /\ b e. ( X ( ClWWalksNOn ` G ) 2 ) ) ) -> ( ( a ++ b ) ` ( N - 2 ) ) = X )
106 1 2clwwlkel 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( a ++ b ) e. ( X C N ) <-> ( ( a ++ b ) e. ( X ( ClWWalksNOn ` G ) N ) /\ ( ( a ++ b ) ` ( N - 2 ) ) = X ) ) )
107 2 106 sylan2 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ b ) e. ( X C N ) <-> ( ( a ++ b ) e. ( X ( ClWWalksNOn ` G ) N ) /\ ( ( a ++ b ) ` ( N - 2 ) ) = X ) ) )
108 107 adantr 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) /\ b e. ( X ( ClWWalksNOn ` G ) 2 ) ) ) -> ( ( a ++ b ) e. ( X C N ) <-> ( ( a ++ b ) e. ( X ( ClWWalksNOn ` G ) N ) /\ ( ( a ++ b ) ` ( N - 2 ) ) = X ) ) )
109 62 105 108 mpbir2and 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) /\ b e. ( X ( ClWWalksNOn ` G ) 2 ) ) ) -> ( a ++ b ) e. ( X C N ) )
110 eleq1 
 |-  ( W = ( a ++ b ) -> ( W e. ( X C N ) <-> ( a ++ b ) e. ( X C N ) ) )
111 109 110 syl5ibrcom 
 |-  ( ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) /\ b e. ( X ( ClWWalksNOn ` G ) 2 ) ) ) -> ( W = ( a ++ b ) -> W e. ( X C N ) ) )
112 111 rexlimdvva 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( E. a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) E. b e. ( X ( ClWWalksNOn ` G ) 2 ) W = ( a ++ b ) -> W e. ( X C N ) ) )
113 53 112 impbid 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. ( X C N ) <-> E. a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) E. b e. ( X ( ClWWalksNOn ` G ) 2 ) W = ( a ++ b ) ) )