Metamath Proof Explorer

Theorem umgrclwwlkge2

Description: A closed walk in a multigraph has a length of at least 2 (because it cannot have a loop). (Contributed by Alexander van der Vekens, 16-Sep-2018) (Revised by AV, 24-Apr-2021)

Ref Expression
Assertion umgrclwwlkge2 
|- ( G e. UMGraph -> ( P e. ( ClWWalks ` G ) -> 2 <_ ( # ` P ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 clwwlkbp 
 |-  ( P e. ( ClWWalks ` G ) -> ( G e. _V /\ P e. Word ( Vtx ` G ) /\ P =/= (/) ) )
3 2 adantl 
 |-  ( ( G e. UMGraph /\ P e. ( ClWWalks ` G ) ) -> ( G e. _V /\ P e. Word ( Vtx ` G ) /\ P =/= (/) ) )
4 lencl 
 |-  ( P e. Word ( Vtx ` G ) -> ( # ` P ) e. NN0 )
5 4 3ad2ant2 
 |-  ( ( G e. _V /\ P e. Word ( Vtx ` G ) /\ P =/= (/) ) -> ( # ` P ) e. NN0 )
6 5 adantl 
 |-  ( ( ( G e. UMGraph /\ P e. ( ClWWalks ` G ) ) /\ ( G e. _V /\ P e. Word ( Vtx ` G ) /\ P =/= (/) ) ) -> ( # ` P ) e. NN0 )
7 hasheq0 
 |-  ( P e. Word ( Vtx ` G ) -> ( ( # ` P ) = 0 <-> P = (/) ) )
8 7 bicomd 
 |-  ( P e. Word ( Vtx ` G ) -> ( P = (/) <-> ( # ` P ) = 0 ) )
9 8 necon3bid 
 |-  ( P e. Word ( Vtx ` G ) -> ( P =/= (/) <-> ( # ` P ) =/= 0 ) )
10 9 biimpd 
 |-  ( P e. Word ( Vtx ` G ) -> ( P =/= (/) -> ( # ` P ) =/= 0 ) )
11 10 a1i 
 |-  ( G e. _V -> ( P e. Word ( Vtx ` G ) -> ( P =/= (/) -> ( # ` P ) =/= 0 ) ) )
12 11 3imp 
 |-  ( ( G e. _V /\ P e. Word ( Vtx ` G ) /\ P =/= (/) ) -> ( # ` P ) =/= 0 )
13 12 adantl 
 |-  ( ( ( G e. UMGraph /\ P e. ( ClWWalks ` G ) ) /\ ( G e. _V /\ P e. Word ( Vtx ` G ) /\ P =/= (/) ) ) -> ( # ` P ) =/= 0 )
14 clwwlk1loop 
 |-  ( ( P e. ( ClWWalks ` G ) /\ ( # ` P ) = 1 ) -> { ( P ` 0 ) , ( P ` 0 ) } e. ( Edg ` G ) )
15 14 expcom 
 |-  ( ( # ` P ) = 1 -> ( P e. ( ClWWalks ` G ) -> { ( P ` 0 ) , ( P ` 0 ) } e. ( Edg ` G ) ) )
16 eqid 
 |-  ( P ` 0 ) = ( P ` 0 )
17 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
18 17 umgredgne 
 |-  ( ( G e. UMGraph /\ { ( P ` 0 ) , ( P ` 0 ) } e. ( Edg ` G ) ) -> ( P ` 0 ) =/= ( P ` 0 ) )
19 eqneqall 
 |-  ( ( P ` 0 ) = ( P ` 0 ) -> ( ( P ` 0 ) =/= ( P ` 0 ) -> ( ( G e. _V /\ P e. Word ( Vtx ` G ) /\ P =/= (/) ) -> ( # ` P ) =/= 1 ) ) )
20 16 18 19 mpsyl 
 |-  ( ( G e. UMGraph /\ { ( P ` 0 ) , ( P ` 0 ) } e. ( Edg ` G ) ) -> ( ( G e. _V /\ P e. Word ( Vtx ` G ) /\ P =/= (/) ) -> ( # ` P ) =/= 1 ) )
21 20 expcom 
 |-  ( { ( P ` 0 ) , ( P ` 0 ) } e. ( Edg ` G ) -> ( G e. UMGraph -> ( ( G e. _V /\ P e. Word ( Vtx ` G ) /\ P =/= (/) ) -> ( # ` P ) =/= 1 ) ) )
22 15 21 syl6 
 |-  ( ( # ` P ) = 1 -> ( P e. ( ClWWalks ` G ) -> ( G e. UMGraph -> ( ( G e. _V /\ P e. Word ( Vtx ` G ) /\ P =/= (/) ) -> ( # ` P ) =/= 1 ) ) ) )
23 22 com23 
 |-  ( ( # ` P ) = 1 -> ( G e. UMGraph -> ( P e. ( ClWWalks ` G ) -> ( ( G e. _V /\ P e. Word ( Vtx ` G ) /\ P =/= (/) ) -> ( # ` P ) =/= 1 ) ) ) )
24 23 imp4c 
 |-  ( ( # ` P ) = 1 -> ( ( ( G e. UMGraph /\ P e. ( ClWWalks ` G ) ) /\ ( G e. _V /\ P e. Word ( Vtx ` G ) /\ P =/= (/) ) ) -> ( # ` P ) =/= 1 ) )
25 neqne 
 |-  ( -. ( # ` P ) = 1 -> ( # ` P ) =/= 1 )
26 25 a1d 
 |-  ( -. ( # ` P ) = 1 -> ( ( ( G e. UMGraph /\ P e. ( ClWWalks ` G ) ) /\ ( G e. _V /\ P e. Word ( Vtx ` G ) /\ P =/= (/) ) ) -> ( # ` P ) =/= 1 ) )
27 24 26 pm2.61i 
 |-  ( ( ( G e. UMGraph /\ P e. ( ClWWalks ` G ) ) /\ ( G e. _V /\ P e. Word ( Vtx ` G ) /\ P =/= (/) ) ) -> ( # ` P ) =/= 1 )
28 6 13 27 3jca 
 |-  ( ( ( G e. UMGraph /\ P e. ( ClWWalks ` G ) ) /\ ( G e. _V /\ P e. Word ( Vtx ` G ) /\ P =/= (/) ) ) -> ( ( # ` P ) e. NN0 /\ ( # ` P ) =/= 0 /\ ( # ` P ) =/= 1 ) )
29 3 28 mpdan 
 |-  ( ( G e. UMGraph /\ P e. ( ClWWalks ` G ) ) -> ( ( # ` P ) e. NN0 /\ ( # ` P ) =/= 0 /\ ( # ` P ) =/= 1 ) )
30 nn0n0n1ge2 
 |-  ( ( ( # ` P ) e. NN0 /\ ( # ` P ) =/= 0 /\ ( # ` P ) =/= 1 ) -> 2 <_ ( # ` P ) )
31 29 30 syl 
 |-  ( ( G e. UMGraph /\ P e. ( ClWWalks ` G ) ) -> 2 <_ ( # ` P ) )
32 31 ex 
 |-  ( G e. UMGraph -> ( P e. ( ClWWalks ` G ) -> 2 <_ ( # ` P ) ) )