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 ⊢ V = Vtx ⁡ G
lfgrn1cycl.i ⊢ I = iEdg ⁡ G
Assertion lfgrn1cycl ⊢ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → F Cycles ⁡ G P → F ≠ 1

Proof

Step Hyp Ref Expression
1 lfgrn1cycl.v ⊢ V = Vtx ⁡ G
2 lfgrn1cycl.i ⊢ I = iEdg ⁡ G
3 cyclprop ⊢ F Cycles ⁡ G P → F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F
4 cycliswlk ⊢ F Cycles ⁡ G P → F Walks ⁡ G P
5 2 1 lfgrwlknloop ⊢ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
6 1nn ⊢ 1 ∈ ℕ
7 eleq1 ⊢ F = 1 → F ∈ ℕ ↔ 1 ∈ ℕ
8 6 7 mpbiri ⊢ F = 1 → F ∈ ℕ
9 lbfzo0 ⊢ 0 ∈ 0 ..^ F ↔ F ∈ ℕ
10 8 9 sylibr ⊢ F = 1 → 0 ∈ 0 ..^ F
11 fveq2 ⊢ k = 0 → P ⁡ k = P ⁡ 0
12 fv0p1e1 ⊢ k = 0 → P ⁡ k + 1 = P ⁡ 1
13 11 12 neeq12d ⊢ k = 0 → P ⁡ k ≠ P ⁡ k + 1 ↔ P ⁡ 0 ≠ P ⁡ 1
14 13 rspcv ⊢ 0 ∈ 0 ..^ F → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 → P ⁡ 0 ≠ P ⁡ 1
15 10 14 syl ⊢ F = 1 → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 → P ⁡ 0 ≠ P ⁡ 1
16 15 impcom ⊢ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ F = 1 → P ⁡ 0 ≠ P ⁡ 1
17 fveq2 ⊢ F = 1 → P ⁡ F = P ⁡ 1
18 17 neeq2d ⊢ F = 1 → P ⁡ 0 ≠ P ⁡ F ↔ P ⁡ 0 ≠ P ⁡ 1
19 18 adantl ⊢ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ F = 1 → P ⁡ 0 ≠ P ⁡ F ↔ P ⁡ 0 ≠ P ⁡ 1
20 16 19 mpbird ⊢ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 ∧ F = 1 → P ⁡ 0 ≠ P ⁡ F
21 20 ex ⊢ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 → F = 1 → P ⁡ 0 ≠ P ⁡ F
22 21 necon2d ⊢ ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1 → P ⁡ 0 = P ⁡ F → F ≠ 1
23 5 22 syl ⊢ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ F Walks ⁡ G P → P ⁡ 0 = P ⁡ F → F ≠ 1
24 23 ex ⊢ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → F Walks ⁡ G P → P ⁡ 0 = P ⁡ F → F ≠ 1
25 24 com13 ⊢ P ⁡ 0 = P ⁡ F → F Walks ⁡ G P → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → F ≠ 1
26 25 adantl ⊢ F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F → F Walks ⁡ G P → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → F ≠ 1
27 3 4 26 sylc ⊢ F Cycles ⁡ G P → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → F ≠ 1
28 27 com12 ⊢ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → F Cycles ⁡ G P → F ≠ 1