Metamath Proof Explorer

Theorem clwwlknonex2e

Description: Extending a closed walk W on vertex X by an additional edge (forth and back) results in a closed walk on vertex X . (Contributed by AV, 17-Apr-2022)

Ref Expression
Hypotheses clwwlknonex2.v 
|- V = ( Vtx ` G )
clwwlknonex2.e 
|- E = ( Edg ` G )
Assertion clwwlknonex2e 
|- ( ( ( 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 ) )

Proof

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