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