wwlks2onv

Description: If a length 3 string represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018) (Proof shortened by AV, 14-Mar-2022)

		Ref	Expression
	Hypothesis	wwlks2onv.v	$⊢ V = Vtx (G)$
	Assertion	wwlks2onv	$⊢ (B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \to (A \in V \land B \in V \land C \in V)$

Proof

Step	Hyp	Ref	Expression
1		wwlks2onv.v	$⊢ V = Vtx (G)$
2	1	wwlksonvtx	$⊢ ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C) \to (A \in V \land C \in V)$
3	2	adantl	$⊢ (B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \to (A \in V \land C \in V)$
4		simprl	$⊢ ((B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \land (A \in V \land C \in V)) \to A \in V$
5		wwlknon	$⊢ ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C) \leftrightarrow (⟨“ A B C ”⟩ \in (2 WWalksN G) \land ⟨“ A B C ”⟩ (0) = A \land ⟨“ A B C ”⟩ (2) = C)$
6		wwlknbp1	$⊢ ⟨“ A B C ”⟩ \in (2 WWalksN G) \to (2 \in ℕ_{0} \land ⟨“ A B C ”⟩ \in Word Vtx (G) \land \|⟨“ A B C ”⟩\| = 2 + 1)$
7		s3fv1	$⊢ B \in U \to ⟨“ A B C ”⟩ (1) = B$
8	7	eqcomd	$⊢ B \in U \to B = ⟨“ A B C ”⟩ (1)$
9	8	adantl	$⊢ (⟨“ A B C ”⟩ \in Word Vtx (G) \land B \in U) \to B = ⟨“ A B C ”⟩ (1)$
10	1	eqcomi	$⊢ Vtx (G) = V$
11	10	wrdeqi	$⊢ Word Vtx (G) = Word V$
12	11	eleq2i	$⊢ ⟨“ A B C ”⟩ \in Word Vtx (G) \leftrightarrow ⟨“ A B C ”⟩ \in Word V$
13	12	biimpi	$⊢ ⟨“ A B C ”⟩ \in Word Vtx (G) \to ⟨“ A B C ”⟩ \in Word V$
14		1ex	$⊢ 1 \in V$
15	14	tpid2	$⊢ 1 \in \{0, 1, 2\}$
16		s3len	$⊢ \|⟨“ A B C ”⟩\| = 3$
17	16	oveq2i	$⊢ (0 ..^\|⟨“ A B C ”⟩\|) = (0 ..^3)$
18		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
19	17 18	eqtri	$⊢ (0 ..^\|⟨“ A B C ”⟩\|) = \{0, 1, 2\}$
20	15 19	eleqtrri	$⊢ 1 \in (0 ..^\|⟨“ A B C ”⟩\|)$
21		wrdsymbcl	$⊢ (⟨“ A B C ”⟩ \in Word V \land 1 \in (0 ..^\|⟨“ A B C ”⟩\|)) \to ⟨“ A B C ”⟩ (1) \in V$
22	13 20 21	sylancl	$⊢ ⟨“ A B C ”⟩ \in Word Vtx (G) \to ⟨“ A B C ”⟩ (1) \in V$
23	22	adantr	$⊢ (⟨“ A B C ”⟩ \in Word Vtx (G) \land B \in U) \to ⟨“ A B C ”⟩ (1) \in V$
24	9 23	eqeltrd	$⊢ (⟨“ A B C ”⟩ \in Word Vtx (G) \land B \in U) \to B \in V$
25	24	ex	$⊢ ⟨“ A B C ”⟩ \in Word Vtx (G) \to (B \in U \to B \in V)$
26	25	3ad2ant2	$⊢ (2 \in ℕ_{0} \land ⟨“ A B C ”⟩ \in Word Vtx (G) \land \|⟨“ A B C ”⟩\| = 2 + 1) \to (B \in U \to B \in V)$
27	6 26	syl	$⊢ ⟨“ A B C ”⟩ \in (2 WWalksN G) \to (B \in U \to B \in V)$
28	27	3ad2ant1	$⊢ (⟨“ A B C ”⟩ \in (2 WWalksN G) \land ⟨“ A B C ”⟩ (0) = A \land ⟨“ A B C ”⟩ (2) = C) \to (B \in U \to B \in V)$
29	5 28	sylbi	$⊢ ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C) \to (B \in U \to B \in V)$
30	29	impcom	$⊢ (B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \to B \in V$
31	30	adantr	$⊢ ((B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \land (A \in V \land C \in V)) \to B \in V$
32		simprr	$⊢ ((B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \land (A \in V \land C \in V)) \to C \in V$
33	4 31 32	3jca	$⊢ ((B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \land (A \in V \land C \in V)) \to (A \in V \land B \in V \land C \in V)$
34	3 33	mpdan	$⊢ (B \in U \land ⟨“ A B C ”⟩ \in (A (2 WWalksNOn G) C)) \to (A \in V \land B \in V \land C \in V)$

Metamath Proof Explorer

Theorem wwlks2onv

Proof