Metamath Proof Explorer

Theorem umgr2cwwk2dif

Description: If a word represents a closed walk of length at least 2 in a multigraph, the first two symbols of the word must be different. (Contributed by Alexander van der Vekens, 17-Jun-2018) (Revised by AV, 30-Apr-2021)

Ref Expression
Assertion umgr2cwwk2dif 
|- ( ( G e. UMGraph /\ N e. ( ZZ>= ` 2 ) /\ W e. ( N ClWWalksN G ) ) -> ( W ` 1 ) =/= ( W ` 0 ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 clwwlknp 
 |-  ( W e. ( N ClWWalksN G ) -> ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
4 simpr 
 |-  ( ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ G e. UMGraph ) -> G e. UMGraph )
5 uz2m1nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. NN )
6 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( N - 1 ) ) <-> ( N - 1 ) e. NN )
7 5 6 sylibr 
 |-  ( N e. ( ZZ>= ` 2 ) -> 0 e. ( 0 ..^ ( N - 1 ) ) )
8 fveq2 
 |-  ( i = 0 -> ( W ` i ) = ( W ` 0 ) )
9 8 adantl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ i = 0 ) -> ( W ` i ) = ( W ` 0 ) )
10 oveq1 
 |-  ( i = 0 -> ( i + 1 ) = ( 0 + 1 ) )
11 10 adantl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ i = 0 ) -> ( i + 1 ) = ( 0 + 1 ) )
12 0p1e1 
 |-  ( 0 + 1 ) = 1
13 11 12 eqtrdi 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ i = 0 ) -> ( i + 1 ) = 1 )
14 13 fveq2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ i = 0 ) -> ( W ` ( i + 1 ) ) = ( W ` 1 ) )
15 9 14 preq12d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ i = 0 ) -> { ( W ` i ) , ( W ` ( i + 1 ) ) } = { ( W ` 0 ) , ( W ` 1 ) } )
16 15 eleq1d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ i = 0 ) -> ( { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) )
17 7 16 rspcdv 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) )
18 17 com12 
 |-  ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( N e. ( ZZ>= ` 2 ) -> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) )
19 18 3ad2ant2 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) -> ( N e. ( ZZ>= ` 2 ) -> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) )
20 19 imp 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ N e. ( ZZ>= ` 2 ) ) -> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) )
21 20 adantr 
 |-  ( ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ G e. UMGraph ) -> { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) )
22 2 umgredgne 
 |-  ( ( G e. UMGraph /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) -> ( W ` 0 ) =/= ( W ` 1 ) )
23 22 necomd 
 |-  ( ( G e. UMGraph /\ { ( W ` 0 ) , ( W ` 1 ) } e. ( Edg ` G ) ) -> ( W ` 1 ) =/= ( W ` 0 ) )
24 4 21 23 syl2anc 
 |-  ( ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ G e. UMGraph ) -> ( W ` 1 ) =/= ( W ` 0 ) )
25 24 exp31 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) -> ( N e. ( ZZ>= ` 2 ) -> ( G e. UMGraph -> ( W ` 1 ) =/= ( W ` 0 ) ) ) )
26 3 25 syl 
 |-  ( W e. ( N ClWWalksN G ) -> ( N e. ( ZZ>= ` 2 ) -> ( G e. UMGraph -> ( W ` 1 ) =/= ( W ` 0 ) ) ) )
27 26 3imp31 
 |-  ( ( G e. UMGraph /\ N e. ( ZZ>= ` 2 ) /\ W e. ( N ClWWalksN G ) ) -> ( W ` 1 ) =/= ( W ` 0 ) )