Theorem cyclnspth

Description: A (non-trivial) cycle is not a simple path. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 31-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Assertion	cyclnspth	$$⊢F\ne \varnothing \to \left(F\mathrm{Cycles}\left(G\right)P\to \neg F\mathrm{SPaths}\left(G\right)P\right)$$

Proof

Step	Hyp	Ref	Expression
1		iscycl	$$⊢F\mathrm{Cycles}\left(G\right)P\leftrightarrow \left(F\mathrm{Paths}\left(G\right)P\wedge P\left(0\right)=P\left(\left|F\right|\right)\right)$$
2		relpths	$$⊢\mathrm{Rel}\mathrm{Paths}\left(G\right)$$
3	2	brrelex1i	$$⊢F\mathrm{Paths}\left(G\right)P\to F\in \mathrm{V}$$
4		hasheq0	$$⊢F\in \mathrm{V}\to \left(\left|F\right|=0\leftrightarrow F=\varnothing \right)$$
5	4	necon3bid	$$⊢F\in \mathrm{V}\to \left(\left|F\right|\ne 0\leftrightarrow F\ne \varnothing \right)$$
6	5	bicomd	$$⊢F\in \mathrm{V}\to \left(F\ne \varnothing \leftrightarrow \left|F\right|\ne 0\right)$$
7	3 6	syl	$$⊢F\mathrm{Paths}\left(G\right)P\to \left(F\ne \varnothing \leftrightarrow \left|F\right|\ne 0\right)$$
8	7	biimpa	$$⊢\left(F\mathrm{Paths}\left(G\right)P\wedge F\ne \varnothing \right)\to \left|F\right|\ne 0$$
9		spthdep	$$⊢\left(F\mathrm{SPaths}\left(G\right)P\wedge \left|F\right|\ne 0\right)\to P\left(0\right)\ne P\left(\left|F\right|\right)$$
10	9	neneqd	$$⊢\left(F\mathrm{SPaths}\left(G\right)P\wedge \left|F\right|\ne 0\right)\to \neg P\left(0\right)=P\left(\left|F\right|\right)$$
11	10	expcom	$$⊢\left|F\right|\ne 0\to \left(F\mathrm{SPaths}\left(G\right)P\to \neg P\left(0\right)=P\left(\left|F\right|\right)\right)$$
12	8 11	syl	$$⊢\left(F\mathrm{Paths}\left(G\right)P\wedge F\ne \varnothing \right)\to \left(F\mathrm{SPaths}\left(G\right)P\to \neg P\left(0\right)=P\left(\left|F\right|\right)\right)$$
13	12	con2d	$$⊢\left(F\mathrm{Paths}\left(G\right)P\wedge F\ne \varnothing \right)\to \left(P\left(0\right)=P\left(\left|F\right|\right)\to \neg F\mathrm{SPaths}\left(G\right)P\right)$$
14	13	impancom	$$⊢\left(F\mathrm{Paths}\left(G\right)P\wedge P\left(0\right)=P\left(\left|F\right|\right)\right)\to \left(F\ne \varnothing \to \neg F\mathrm{SPaths}\left(G\right)P\right)$$
15	1 14	sylbi	$$⊢F\mathrm{Cycles}\left(G\right)P\to \left(F\ne \varnothing \to \neg F\mathrm{SPaths}\left(G\right)P\right)$$
16	15	com12	$$⊢F\ne \varnothing \to \left(F\mathrm{Cycles}\left(G\right)P\to \neg F\mathrm{SPaths}\left(G\right)P\right)$$