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 ( 𝐺 ∈ UMGraph → ( 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) → 2 ≤ ( ♯ ‘ 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 1 clwwlkbp ⊢ ( 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) )
3 2 adantl ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) ) → ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) )
4 lencl ⊢ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
5 4 3ad2ant2 ⊢ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
6 5 adantl ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) ) → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
7 hasheq0 ⊢ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑃 ) = 0 ↔ 𝑃 = ∅ ) )
8 7 bicomd ⊢ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑃 = ∅ ↔ ( ♯ ‘ 𝑃 ) = 0 ) )
9 8 necon3bid ⊢ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑃 ≠ ∅ ↔ ( ♯ ‘ 𝑃 ) ≠ 0 ) )
10 9 biimpd ⊢ ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑃 ≠ ∅ → ( ♯ ‘ 𝑃 ) ≠ 0 ) )
11 10 a1i ⊢ ( 𝐺 ∈ V → ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑃 ≠ ∅ → ( ♯ ‘ 𝑃 ) ≠ 0 ) ) )
12 11 3imp ⊢ ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) → ( ♯ ‘ 𝑃 ) ≠ 0 )
13 12 adantl ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) ) → ( ♯ ‘ 𝑃 ) ≠ 0 )
14 clwwlk1loop ⊢ ( ( 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑃 ) = 1 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
15 14 expcom ⊢ ( ( ♯ ‘ 𝑃 ) = 1 → ( 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
16 eqid ⊢ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 )
17 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
18 17 umgredgne ⊢ ( ( 𝐺 ∈ UMGraph ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 0 ) )
19 eqneqall ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 0 ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 0 ) → ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) → ( ♯ ‘ 𝑃 ) ≠ 1 ) ) )
20 16 18 19 mpsyl ⊢ ( ( 𝐺 ∈ UMGraph ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) → ( ♯ ‘ 𝑃 ) ≠ 1 ) )
21 20 expcom ⊢ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ( 𝐺 ∈ UMGraph → ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) → ( ♯ ‘ 𝑃 ) ≠ 1 ) ) )
22 15 21 syl6 ⊢ ( ( ♯ ‘ 𝑃 ) = 1 → ( 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝐺 ∈ UMGraph → ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) → ( ♯ ‘ 𝑃 ) ≠ 1 ) ) ) )
23 22 com23 ⊢ ( ( ♯ ‘ 𝑃 ) = 1 → ( 𝐺 ∈ UMGraph → ( 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) → ( ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) → ( ♯ ‘ 𝑃 ) ≠ 1 ) ) ) )
24 23 imp4c ⊢ ( ( ♯ ‘ 𝑃 ) = 1 → ( ( ( 𝐺 ∈ UMGraph ∧ 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) ) → ( ♯ ‘ 𝑃 ) ≠ 1 ) )
25 neqne ⊢ ( ¬ ( ♯ ‘ 𝑃 ) = 1 → ( ♯ ‘ 𝑃 ) ≠ 1 )
26 25 a1d ⊢ ( ¬ ( ♯ ‘ 𝑃 ) = 1 → ( ( ( 𝐺 ∈ UMGraph ∧ 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) ) → ( ♯ ‘ 𝑃 ) ≠ 1 ) )
27 24 26 pm2.61i ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) ) → ( ♯ ‘ 𝑃 ) ≠ 1 )
28 6 13 27 3jca ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( 𝐺 ∈ V ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑃 ≠ ∅ ) ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ≠ 0 ∧ ( ♯ ‘ 𝑃 ) ≠ 1 ) )
29 3 28 mpdan ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ≠ 0 ∧ ( ♯ ‘ 𝑃 ) ≠ 1 ) )
30 nn0n0n1ge2 ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ≠ 0 ∧ ( ♯ ‘ 𝑃 ) ≠ 1 ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
31 29 30 syl ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
32 31 ex ⊢ ( 𝐺 ∈ UMGraph → ( 𝑃 ∈ ( ClWWalks ‘ 𝐺 ) → 2 ≤ ( ♯ ‘ 𝑃 ) ) )