lfgrwlkprop

Description: Two adjacent vertices in a walk are different in a loop-free graph. (Contributed by AV, 28-Jan-2021)

		Ref	Expression
	Hypothesis	lfgrwlkprop.i	$⊢ I = iEdg (G)$
	Assertion	lfgrwlkprop	$⊢ (F Walks (G) P \land I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}) \to \forall k \in (0 ..^\|F\|) P (k) \neq P (k + 1)$

Proof

Step	Hyp	Ref	Expression
1		lfgrwlkprop.i	$⊢ I = iEdg (G)$
2		wlkv	$⊢ F Walks (G) P \to (G \in V \land F \in V \land P \in V)$
3		eqid	$⊢ Vtx (G) = Vtx (G)$
4	3 1	iswlk	$⊢ (G \in V \land F \in V \land P \in V) \to (F Walks (G) P \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))))$
5	2 4	syl	$⊢ F Walks (G) P \to (F Walks (G) P \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))))$
6		ifptru	$⊢ P (k) = P (k + 1) \to (if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \leftrightarrow I (F (k)) = \{P (k)\})$
7	6	adantr	$⊢ (P (k) = P (k + 1) \land (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}) \land k \in (0 ..^\|F\|))) \to (if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \leftrightarrow I (F (k)) = \{P (k)\})$
8		simplr	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}) \land k \in (0 ..^\|F\|)) \to I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}$
9		wrdsymbcl	$⊢ (F \in Word dom I \land k \in (0 ..^\|F\|)) \to F (k) \in dom I$
10	9	ad4ant14	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}) \land k \in (0 ..^\|F\|)) \to F (k) \in dom I$
11	8 10	ffvelcdmd	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}) \land k \in (0 ..^\|F\|)) \to I (F (k)) \in \{x \in 𝒫 V \| 2 \leq \|x\|\}$
12		fveq2	$⊢ x = I (F (k)) \to \|x\| = \|I (F (k))\|$
13	12	breq2d	$⊢ x = I (F (k)) \to (2 \leq \|x\| \leftrightarrow 2 \leq \|I (F (k))\|)$
14	13	elrab	$⊢ I (F (k)) \in \{x \in 𝒫 V \| 2 \leq \|x\|\} \leftrightarrow (I (F (k)) \in 𝒫 V \land 2 \leq \|I (F (k))\|)$
15		fveq2	$⊢ I (F (k)) = \{P (k)\} \to \|I (F (k))\| = \|\{P (k)\}\|$
16	15	breq2d	$⊢ I (F (k)) = \{P (k)\} \to (2 \leq \|I (F (k))\| \leftrightarrow 2 \leq \|\{P (k)\}\|)$
17		fvex	$⊢ P (k) \in V$
18		hashsng	$⊢ P (k) \in V \to \|\{P (k)\}\| = 1$
19	17 18	ax-mp	$⊢ \|\{P (k)\}\| = 1$
20	19	breq2i	$⊢ 2 \leq \|\{P (k)\}\| \leftrightarrow 2 \leq 1$
21		1lt2	$⊢ 1 < 2$
22		1re	$⊢ 1 \in ℝ$
23		2re	$⊢ 2 \in ℝ$
24	22 23	ltnlei	$⊢ 1 < 2 \leftrightarrow \neg 2 \leq 1$
25		pm2.21	$⊢ \neg 2 \leq 1 \to (2 \leq 1 \to P (k) \neq P (k + 1))$
26	24 25	sylbi	$⊢ 1 < 2 \to (2 \leq 1 \to P (k) \neq P (k + 1))$
27	21 26	ax-mp	$⊢ 2 \leq 1 \to P (k) \neq P (k + 1)$
28	20 27	sylbi	$⊢ 2 \leq \|\{P (k)\}\| \to P (k) \neq P (k + 1)$
29	16 28	syl6bi	$⊢ I (F (k)) = \{P (k)\} \to (2 \leq \|I (F (k))\| \to P (k) \neq P (k + 1))$
30	29	com12	$⊢ 2 \leq \|I (F (k))\| \to (I (F (k)) = \{P (k)\} \to P (k) \neq P (k + 1))$
31	30	adantl	$⊢ (I (F (k)) \in 𝒫 V \land 2 \leq \|I (F (k))\|) \to (I (F (k)) = \{P (k)\} \to P (k) \neq P (k + 1))$
32	31	a1i	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}) \land k \in (0 ..^\|F\|)) \to ((I (F (k)) \in 𝒫 V \land 2 \leq \|I (F (k))\|) \to (I (F (k)) = \{P (k)\} \to P (k) \neq P (k + 1)))$
33	14 32	biimtrid	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}) \land k \in (0 ..^\|F\|)) \to (I (F (k)) \in \{x \in 𝒫 V \| 2 \leq \|x\|\} \to (I (F (k)) = \{P (k)\} \to P (k) \neq P (k + 1)))$
34	11 33	mpd	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}) \land k \in (0 ..^\|F\|)) \to (I (F (k)) = \{P (k)\} \to P (k) \neq P (k + 1))$
35	34	adantl	$⊢ (P (k) = P (k + 1) \land (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}) \land k \in (0 ..^\|F\|))) \to (I (F (k)) = \{P (k)\} \to P (k) \neq P (k + 1))$
36	7 35	sylbid	$⊢ (P (k) = P (k + 1) \land (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}) \land k \in (0 ..^\|F\|))) \to (if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \to P (k) \neq P (k + 1))$
37	36	ex	$⊢ P (k) = P (k + 1) \to ((((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}) \land k \in (0 ..^\|F\|)) \to (if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \to P (k) \neq P (k + 1)))$
38		neqne	$⊢ \neg P (k) = P (k + 1) \to P (k) \neq P (k + 1)$
39	38	2a1d	$⊢ \neg P (k) = P (k + 1) \to ((((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}) \land k \in (0 ..^\|F\|)) \to (if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \to P (k) \neq P (k + 1)))$
40	37 39	pm2.61i	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}) \land k \in (0 ..^\|F\|)) \to (if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \to P (k) \neq P (k + 1))$
41	40	ralimdva	$⊢ ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}) \to (\forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \to \forall k \in (0 ..^\|F\|) P (k) \neq P (k + 1))$
42	41	ex	$⊢ (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to (I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\} \to (\forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \to \forall k \in (0 ..^\|F\|) P (k) \neq P (k + 1)))$
43	42	com23	$⊢ (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to (\forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \to (I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\} \to \forall k \in (0 ..^\|F\|) P (k) \neq P (k + 1)))$
44	43	3impia	$⊢ (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))) \to (I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\} \to \forall k \in (0 ..^\|F\|) P (k) \neq P (k + 1))$
45	5 44	syl6bi	$⊢ F Walks (G) P \to (F Walks (G) P \to (I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\} \to \forall k \in (0 ..^\|F\|) P (k) \neq P (k + 1)))$
46	45	pm2.43i	$⊢ F Walks (G) P \to (I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\} \to \forall k \in (0 ..^\|F\|) P (k) \neq P (k + 1))$
47	46	imp	$⊢ (F Walks (G) P \land I : dom I ⟶ \{x \in 𝒫 V \| 2 \leq \|x\|\}) \to \forall k \in (0 ..^\|F\|) P (k) \neq P (k + 1)$

Metamath Proof Explorer

Theorem lfgrwlkprop

Proof