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 ) )