Metamath Proof Explorer

Theorem lfgrn1cycl

Description: In a loop-free graph there are no cycles with length 1 (consisting of one edge). (Contributed by Alexander van der Vekens, 7-Nov-2017) (Revised by AV, 2-Feb-2021)

Ref Expression
Hypotheses lfgrn1cycl.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
lfgrn1cycl.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion lfgrn1cycl ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ≠ 1 ) )

Proof

Step Hyp Ref Expression
1 lfgrn1cycl.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 lfgrn1cycl.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 cyclprop ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
4 cycliswlk ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
5 2 1 lfgrwlknloop ⊢ ( ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
6 1nn ⊢ 1 ∈ ℕ
7 eleq1 ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ ↔ 1 ∈ ℕ ) )
8 6 7 mpbiri ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( ♯ ‘ 𝐹 ) ∈ ℕ )
9 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( ♯ ‘ 𝐹 ) ∈ ℕ )
10 8 9 sylibr ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
11 fveq2 ⊢ ( 𝑘 = 0 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 0 ) )
12 fv0p1e1 ⊢ ( 𝑘 = 0 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 1 ) )
13 11 12 neeq12d ⊢ ( 𝑘 = 0 → ( ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
14 13 rspcv ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
15 10 14 syl ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
16 15 impcom ⊢ ( ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ♯ ‘ 𝐹 ) = 1 ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) )
17 fveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 1 ) )
18 17 neeq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
19 18 adantl ⊢ ( ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ♯ ‘ 𝐹 ) = 1 ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) )
20 16 19 mpbird ⊢ ( ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ♯ ‘ 𝐹 ) = 1 ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
21 20 ex ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( ( ♯ ‘ 𝐹 ) = 1 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
22 21 necon2d ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ≠ 1 ) )
23 5 22 syl ⊢ ( ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ≠ 1 ) )
24 23 ex ⊢ ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ≠ 1 ) ) )
25 24 com13 ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → ( ♯ ‘ 𝐹 ) ≠ 1 ) ) )
26 25 adantl ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → ( ♯ ‘ 𝐹 ) ≠ 1 ) ) )
27 3 4 26 sylc ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → ( ♯ ‘ 𝐹 ) ≠ 1 ) )
28 27 com12 ⊢ ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ≠ 1 ) )