Step |
Hyp |
Ref |
Expression |
1 |
|
clwwlknonex2.v |
|- V = ( Vtx ` G ) |
2 |
|
clwwlknonex2.e |
|- E = ( Edg ` G ) |
3 |
1 2
|
clwwlknonex2 |
|- ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ { X , Y } e. E /\ W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( N ClWWalksN G ) ) |
4 |
|
isclwwlknon |
|- ( W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) <-> ( W e. ( ( N - 2 ) ClWWalksN G ) /\ ( W ` 0 ) = X ) ) |
5 |
|
isclwwlkn |
|- ( W e. ( ( N - 2 ) ClWWalksN G ) <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = ( N - 2 ) ) ) |
6 |
1
|
clwwlkbp |
|- ( W e. ( ClWWalks ` G ) -> ( G e. _V /\ W e. Word V /\ W =/= (/) ) ) |
7 |
6
|
simp2d |
|- ( W e. ( ClWWalks ` G ) -> W e. Word V ) |
8 |
|
clwwlkgt0 |
|- ( W e. ( ClWWalks ` G ) -> 0 < ( # ` W ) ) |
9 |
7 8
|
jca |
|- ( W e. ( ClWWalks ` G ) -> ( W e. Word V /\ 0 < ( # ` W ) ) ) |
10 |
9
|
adantr |
|- ( ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = ( N - 2 ) ) -> ( W e. Word V /\ 0 < ( # ` W ) ) ) |
11 |
5 10
|
sylbi |
|- ( W e. ( ( N - 2 ) ClWWalksN G ) -> ( W e. Word V /\ 0 < ( # ` W ) ) ) |
12 |
11
|
ad2antrl |
|- ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( ( N - 2 ) ClWWalksN G ) /\ ( W ` 0 ) = X ) ) -> ( W e. Word V /\ 0 < ( # ` W ) ) ) |
13 |
|
ccat2s1fst |
|- ( ( W e. Word V /\ 0 < ( # ` W ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) = ( W ` 0 ) ) |
14 |
12 13
|
syl |
|- ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( ( N - 2 ) ClWWalksN G ) /\ ( W ` 0 ) = X ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) = ( W ` 0 ) ) |
15 |
|
simprr |
|- ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( ( N - 2 ) ClWWalksN G ) /\ ( W ` 0 ) = X ) ) -> ( W ` 0 ) = X ) |
16 |
14 15
|
eqtrd |
|- ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( W e. ( ( N - 2 ) ClWWalksN G ) /\ ( W ` 0 ) = X ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) = X ) |
17 |
16
|
ex |
|- ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( W e. ( ( N - 2 ) ClWWalksN G ) /\ ( W ` 0 ) = X ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) = X ) ) |
18 |
4 17
|
syl5bi |
|- ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) = X ) ) |
19 |
18
|
a1d |
|- ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( { X , Y } e. E -> ( W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) = X ) ) ) |
20 |
19
|
3imp |
|- ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ { X , Y } e. E /\ W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) = X ) |
21 |
|
isclwwlknon |
|- ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( X ( ClWWalksNOn ` G ) N ) <-> ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( N ClWWalksN G ) /\ ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) = X ) ) |
22 |
3 20 21
|
sylanbrc |
|- ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ { X , Y } e. E /\ W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( X ( ClWWalksNOn ` G ) N ) ) |