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 ) ) ) |