# 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}=\mathrm{Vtx}\left({G}\right)$
lfgrn1cycl.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
Assertion lfgrn1cycl ${⊢}{I}:\mathrm{dom}{I}⟶\left\{{x}\in 𝒫{V}|2\le \left|{x}\right|\right\}\to \left({F}\mathrm{Cycles}\left({G}\right){P}\to \left|{F}\right|\ne 1\right)$

### Proof

Step Hyp Ref Expression
1 lfgrn1cycl.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 lfgrn1cycl.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3 cyclprop ${⊢}{F}\mathrm{Cycles}\left({G}\right){P}\to \left({F}\mathrm{Paths}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)$
4 cycliswlk ${⊢}{F}\mathrm{Cycles}\left({G}\right){P}\to {F}\mathrm{Walks}\left({G}\right){P}$
5 2 1 lfgrwlknloop ${⊢}\left({I}:\mathrm{dom}{I}⟶\left\{{x}\in 𝒫{V}|2\le \left|{x}\right|\right\}\wedge {F}\mathrm{Walks}\left({G}\right){P}\right)\to \forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{P}\left({k}\right)\ne {P}\left({k}+1\right)$
6 1nn ${⊢}1\in ℕ$
7 eleq1 ${⊢}\left|{F}\right|=1\to \left(\left|{F}\right|\in ℕ↔1\in ℕ\right)$
8 6 7 mpbiri ${⊢}\left|{F}\right|=1\to \left|{F}\right|\in ℕ$
9 lbfzo0 ${⊢}0\in \left(0..^\left|{F}\right|\right)↔\left|{F}\right|\in ℕ$
10 8 9 sylibr ${⊢}\left|{F}\right|=1\to 0\in \left(0..^\left|{F}\right|\right)$
11 fveq2 ${⊢}{k}=0\to {P}\left({k}\right)={P}\left(0\right)$
12 fv0p1e1 ${⊢}{k}=0\to {P}\left({k}+1\right)={P}\left(1\right)$
13 11 12 neeq12d ${⊢}{k}=0\to \left({P}\left({k}\right)\ne {P}\left({k}+1\right)↔{P}\left(0\right)\ne {P}\left(1\right)\right)$
14 13 rspcv ${⊢}0\in \left(0..^\left|{F}\right|\right)\to \left(\forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{P}\left({k}\right)\ne {P}\left({k}+1\right)\to {P}\left(0\right)\ne {P}\left(1\right)\right)$
15 10 14 syl ${⊢}\left|{F}\right|=1\to \left(\forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{P}\left({k}\right)\ne {P}\left({k}+1\right)\to {P}\left(0\right)\ne {P}\left(1\right)\right)$
16 15 impcom ${⊢}\left(\forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{P}\left({k}\right)\ne {P}\left({k}+1\right)\wedge \left|{F}\right|=1\right)\to {P}\left(0\right)\ne {P}\left(1\right)$
17 fveq2 ${⊢}\left|{F}\right|=1\to {P}\left(\left|{F}\right|\right)={P}\left(1\right)$
18 17 neeq2d ${⊢}\left|{F}\right|=1\to \left({P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)↔{P}\left(0\right)\ne {P}\left(1\right)\right)$
19 18 adantl ${⊢}\left(\forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{P}\left({k}\right)\ne {P}\left({k}+1\right)\wedge \left|{F}\right|=1\right)\to \left({P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)↔{P}\left(0\right)\ne {P}\left(1\right)\right)$
20 16 19 mpbird ${⊢}\left(\forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{P}\left({k}\right)\ne {P}\left({k}+1\right)\wedge \left|{F}\right|=1\right)\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)$
21 20 ex ${⊢}\forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{P}\left({k}\right)\ne {P}\left({k}+1\right)\to \left(\left|{F}\right|=1\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)\right)$
22 21 necon2d ${⊢}\forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}{P}\left({k}\right)\ne {P}\left({k}+1\right)\to \left({P}\left(0\right)={P}\left(\left|{F}\right|\right)\to \left|{F}\right|\ne 1\right)$
23 5 22 syl ${⊢}\left({I}:\mathrm{dom}{I}⟶\left\{{x}\in 𝒫{V}|2\le \left|{x}\right|\right\}\wedge {F}\mathrm{Walks}\left({G}\right){P}\right)\to \left({P}\left(0\right)={P}\left(\left|{F}\right|\right)\to \left|{F}\right|\ne 1\right)$
24 23 ex ${⊢}{I}:\mathrm{dom}{I}⟶\left\{{x}\in 𝒫{V}|2\le \left|{x}\right|\right\}\to \left({F}\mathrm{Walks}\left({G}\right){P}\to \left({P}\left(0\right)={P}\left(\left|{F}\right|\right)\to \left|{F}\right|\ne 1\right)\right)$
25 24 com13 ${⊢}{P}\left(0\right)={P}\left(\left|{F}\right|\right)\to \left({F}\mathrm{Walks}\left({G}\right){P}\to \left({I}:\mathrm{dom}{I}⟶\left\{{x}\in 𝒫{V}|2\le \left|{x}\right|\right\}\to \left|{F}\right|\ne 1\right)\right)$
26 25 adantl ${⊢}\left({F}\mathrm{Paths}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left({F}\mathrm{Walks}\left({G}\right){P}\to \left({I}:\mathrm{dom}{I}⟶\left\{{x}\in 𝒫{V}|2\le \left|{x}\right|\right\}\to \left|{F}\right|\ne 1\right)\right)$
27 3 4 26 sylc ${⊢}{F}\mathrm{Cycles}\left({G}\right){P}\to \left({I}:\mathrm{dom}{I}⟶\left\{{x}\in 𝒫{V}|2\le \left|{x}\right|\right\}\to \left|{F}\right|\ne 1\right)$
28 27 com12 ${⊢}{I}:\mathrm{dom}{I}⟶\left\{{x}\in 𝒫{V}|2\le \left|{x}\right|\right\}\to \left({F}\mathrm{Cycles}\left({G}\right){P}\to \left|{F}\right|\ne 1\right)$