elwwlks2

Description: A walk of length 2 between two vertices as length 3 string in a pseudograph. (Contributed by Alexander van der Vekens, 21-Feb-2018) (Revised by AV, 17-May-2021) (Proof shortened by AV, 14-Mar-2022)

		Ref	Expression
	Hypothesis	elwwlks2.v	$⊢ V = Vtx (G)$
	Assertion	elwwlks2	$⊢ G \in UPGraph \to (W \in (2 WWalksN G) \leftrightarrow \exists a \in V \exists b \in V \exists c \in V (W = ⟨“ a b c ”⟩ \land \exists f \exists p (f Walks (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))))$

Proof

Step	Hyp	Ref	Expression
1		elwwlks2.v	$⊢ V = Vtx (G)$
2	1	wwlksnwwlksnon	$⊢ W \in (2 WWalksN G) \leftrightarrow \exists a \in V \exists c \in V W \in (a (2 WWalksNOn G) c)$
3	2	a1i	$⊢ G \in UPGraph \to (W \in (2 WWalksN G) \leftrightarrow \exists a \in V \exists c \in V W \in (a (2 WWalksNOn G) c))$
4	1	elwwlks2on	$⊢ (G \in UPGraph \land a \in V \land c \in V) \to (W \in (a (2 WWalksNOn G) c) \leftrightarrow \exists b \in V (W = ⟨“ a b c ”⟩ \land \exists f (f Walks (G) W \land \|f\| = 2)))$
5	4	3expb	$⊢ (G \in UPGraph \land (a \in V \land c \in V)) \to (W \in (a (2 WWalksNOn G) c) \leftrightarrow \exists b \in V (W = ⟨“ a b c ”⟩ \land \exists f (f Walks (G) W \land \|f\| = 2)))$
6	5	2rexbidva	$⊢ G \in UPGraph \to (\exists a \in V \exists c \in V W \in (a (2 WWalksNOn G) c) \leftrightarrow \exists a \in V \exists c \in V \exists b \in V (W = ⟨“ a b c ”⟩ \land \exists f (f Walks (G) W \land \|f\| = 2)))$
7		rexcom	$⊢ \exists c \in V \exists b \in V (W = ⟨“ a b c ”⟩ \land \exists f (f Walks (G) W \land \|f\| = 2)) \leftrightarrow \exists b \in V \exists c \in V (W = ⟨“ a b c ”⟩ \land \exists f (f Walks (G) W \land \|f\| = 2))$
8		s3cli	$⊢ ⟨“ a b c ”⟩ \in Word V$
9	8	a1i	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to ⟨“ a b c ”⟩ \in Word V$
10		simplr	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \land p = ⟨“ a b c ”⟩) \to W = ⟨“ a b c ”⟩$
11		simpr	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \land p = ⟨“ a b c ”⟩) \to p = ⟨“ a b c ”⟩$
12	10 11	eqtr4d	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \land p = ⟨“ a b c ”⟩) \to W = p$
13	12	breq2d	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \land p = ⟨“ a b c ”⟩) \to (f Walks (G) W \leftrightarrow f Walks (G) p)$
14	13	biimpd	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \land p = ⟨“ a b c ”⟩) \to (f Walks (G) W \to f Walks (G) p)$
15	14	com12	$⊢ f Walks (G) W \to (((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \land p = ⟨“ a b c ”⟩) \to f Walks (G) p)$
16	15	adantr	$⊢ (f Walks (G) W \land \|f\| = 2) \to (((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \land p = ⟨“ a b c ”⟩) \to f Walks (G) p)$
17	16	impcom	$⊢ (((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \land p = ⟨“ a b c ”⟩) \land (f Walks (G) W \land \|f\| = 2)) \to f Walks (G) p$
18		simprr	$⊢ (((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \land p = ⟨“ a b c ”⟩) \land (f Walks (G) W \land \|f\| = 2)) \to \|f\| = 2$
19		vex	$⊢ a \in V$
20		s3fv0	$⊢ a \in V \to ⟨“ a b c ”⟩ (0) = a$
21	20	eqcomd	$⊢ a \in V \to a = ⟨“ a b c ”⟩ (0)$
22	19 21	mp1i	$⊢ p = ⟨“ a b c ”⟩ \to a = ⟨“ a b c ”⟩ (0)$
23		fveq1	$⊢ p = ⟨“ a b c ”⟩ \to p (0) = ⟨“ a b c ”⟩ (0)$
24	22 23	eqtr4d	$⊢ p = ⟨“ a b c ”⟩ \to a = p (0)$
25		vex	$⊢ b \in V$
26		s3fv1	$⊢ b \in V \to ⟨“ a b c ”⟩ (1) = b$
27	26	eqcomd	$⊢ b \in V \to b = ⟨“ a b c ”⟩ (1)$
28	25 27	mp1i	$⊢ p = ⟨“ a b c ”⟩ \to b = ⟨“ a b c ”⟩ (1)$
29		fveq1	$⊢ p = ⟨“ a b c ”⟩ \to p (1) = ⟨“ a b c ”⟩ (1)$
30	28 29	eqtr4d	$⊢ p = ⟨“ a b c ”⟩ \to b = p (1)$
31		vex	$⊢ c \in V$
32		s3fv2	$⊢ c \in V \to ⟨“ a b c ”⟩ (2) = c$
33	32	eqcomd	$⊢ c \in V \to c = ⟨“ a b c ”⟩ (2)$
34	31 33	mp1i	$⊢ p = ⟨“ a b c ”⟩ \to c = ⟨“ a b c ”⟩ (2)$
35		fveq1	$⊢ p = ⟨“ a b c ”⟩ \to p (2) = ⟨“ a b c ”⟩ (2)$
36	34 35	eqtr4d	$⊢ p = ⟨“ a b c ”⟩ \to c = p (2)$
37	24 30 36	3jca	$⊢ p = ⟨“ a b c ”⟩ \to (a = p (0) \land b = p (1) \land c = p (2))$
38	37	adantl	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \land p = ⟨“ a b c ”⟩) \to (a = p (0) \land b = p (1) \land c = p (2))$
39	38	adantr	$⊢ (((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \land p = ⟨“ a b c ”⟩) \land (f Walks (G) W \land \|f\| = 2)) \to (a = p (0) \land b = p (1) \land c = p (2))$
40	17 18 39	3jca	$⊢ (((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \land p = ⟨“ a b c ”⟩) \land (f Walks (G) W \land \|f\| = 2)) \to (f Walks (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))$
41	40	ex	$⊢ ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \land p = ⟨“ a b c ”⟩) \to ((f Walks (G) W \land \|f\| = 2) \to (f Walks (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))))$
42	9 41	spcimedv	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to ((f Walks (G) W \land \|f\| = 2) \to \exists p (f Walks (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))))$
43		wlklenvp1	$⊢ f Walks (G) p \to \|p\| = \|f\| + 1$
44		simpl	$⊢ (\|p\| = \|f\| + 1 \land \|f\| = 2) \to \|p\| = \|f\| + 1$
45		oveq1	$⊢ \|f\| = 2 \to \|f\| + 1 = 2 + 1$
46	45	adantl	$⊢ (\|p\| = \|f\| + 1 \land \|f\| = 2) \to \|f\| + 1 = 2 + 1$
47	44 46	eqtrd	$⊢ (\|p\| = \|f\| + 1 \land \|f\| = 2) \to \|p\| = 2 + 1$
48	47	adantl	$⊢ (f Walks (G) p \land (\|p\| = \|f\| + 1 \land \|f\| = 2)) \to \|p\| = 2 + 1$
49		2p1e3	$⊢ 2 + 1 = 3$
50	48 49	eqtrdi	$⊢ (f Walks (G) p \land (\|p\| = \|f\| + 1 \land \|f\| = 2)) \to \|p\| = 3$
51	50	exp32	$⊢ f Walks (G) p \to (\|p\| = \|f\| + 1 \to (\|f\| = 2 \to \|p\| = 3))$
52	43 51	mpd	$⊢ f Walks (G) p \to (\|f\| = 2 \to \|p\| = 3)$
53	52	adantr	$⊢ (f Walks (G) p \land (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩)) \to (\|f\| = 2 \to \|p\| = 3)$
54	53	imp	$⊢ ((f Walks (G) p \land (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩)) \land \|f\| = 2) \to \|p\| = 3$
55		eqcom	$⊢ a = p (0) \leftrightarrow p (0) = a$
56	55	biimpi	$⊢ a = p (0) \to p (0) = a$
57		eqcom	$⊢ b = p (1) \leftrightarrow p (1) = b$
58	57	biimpi	$⊢ b = p (1) \to p (1) = b$
59		eqcom	$⊢ c = p (2) \leftrightarrow p (2) = c$
60	59	biimpi	$⊢ c = p (2) \to p (2) = c$
61	56 58 60	3anim123i	$⊢ (a = p (0) \land b = p (1) \land c = p (2)) \to (p (0) = a \land p (1) = b \land p (2) = c)$
62	54 61	anim12i	$⊢ (((f Walks (G) p \land (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩)) \land \|f\| = 2) \land (a = p (0) \land b = p (1) \land c = p (2))) \to (\|p\| = 3 \land (p (0) = a \land p (1) = b \land p (2) = c))$
63	1	wlkpwrd	$⊢ f Walks (G) p \to p \in Word V$
64		simpr	$⊢ (G \in UPGraph \land a \in V) \to a \in V$
65	64	anim1i	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to (a \in V \land (b \in V \land c \in V))$
66		3anass	$⊢ (a \in V \land b \in V \land c \in V) \leftrightarrow (a \in V \land (b \in V \land c \in V))$
67	65 66	sylibr	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to (a \in V \land b \in V \land c \in V)$
68	67	adantr	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to (a \in V \land b \in V \land c \in V)$
69	63 68	anim12i	$⊢ (f Walks (G) p \land (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩)) \to (p \in Word V \land (a \in V \land b \in V \land c \in V))$
70	69	ad2antrr	$⊢ (((f Walks (G) p \land (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩)) \land \|f\| = 2) \land (a = p (0) \land b = p (1) \land c = p (2))) \to (p \in Word V \land (a \in V \land b \in V \land c \in V))$
71		eqwrds3	$⊢ (p \in Word V \land (a \in V \land b \in V \land c \in V)) \to (p = ⟨“ a b c ”⟩ \leftrightarrow (\|p\| = 3 \land (p (0) = a \land p (1) = b \land p (2) = c)))$
72	70 71	syl	$⊢ (((f Walks (G) p \land (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩)) \land \|f\| = 2) \land (a = p (0) \land b = p (1) \land c = p (2))) \to (p = ⟨“ a b c ”⟩ \leftrightarrow (\|p\| = 3 \land (p (0) = a \land p (1) = b \land p (2) = c)))$
73	62 72	mpbird	$⊢ (((f Walks (G) p \land (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩)) \land \|f\| = 2) \land (a = p (0) \land b = p (1) \land c = p (2))) \to p = ⟨“ a b c ”⟩$
74		simprr	$⊢ (f Walks (G) p \land (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩)) \to W = ⟨“ a b c ”⟩$
75	74	ad2antrr	$⊢ (((f Walks (G) p \land (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩)) \land \|f\| = 2) \land (a = p (0) \land b = p (1) \land c = p (2))) \to W = ⟨“ a b c ”⟩$
76	73 75	eqtr4d	$⊢ (((f Walks (G) p \land (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩)) \land \|f\| = 2) \land (a = p (0) \land b = p (1) \land c = p (2))) \to p = W$
77	76	breq2d	$⊢ (((f Walks (G) p \land (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩)) \land \|f\| = 2) \land (a = p (0) \land b = p (1) \land c = p (2))) \to (f Walks (G) p \leftrightarrow f Walks (G) W)$
78	77	biimpd	$⊢ (((f Walks (G) p \land (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩)) \land \|f\| = 2) \land (a = p (0) \land b = p (1) \land c = p (2))) \to (f Walks (G) p \to f Walks (G) W)$
79		simplr	$⊢ (((f Walks (G) p \land (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩)) \land \|f\| = 2) \land (a = p (0) \land b = p (1) \land c = p (2))) \to \|f\| = 2$
80	78 79	jctird	$⊢ (((f Walks (G) p \land (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩)) \land \|f\| = 2) \land (a = p (0) \land b = p (1) \land c = p (2))) \to (f Walks (G) p \to (f Walks (G) W \land \|f\| = 2))$
81	80	exp41	$⊢ f Walks (G) p \to ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to (\|f\| = 2 \to ((a = p (0) \land b = p (1) \land c = p (2)) \to (f Walks (G) p \to (f Walks (G) W \land \|f\| = 2)))))$
82	81	com25	$⊢ f Walks (G) p \to (f Walks (G) p \to (\|f\| = 2 \to ((a = p (0) \land b = p (1) \land c = p (2)) \to ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to (f Walks (G) W \land \|f\| = 2)))))$
83	82	pm2.43i	$⊢ f Walks (G) p \to (\|f\| = 2 \to ((a = p (0) \land b = p (1) \land c = p (2)) \to ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to (f Walks (G) W \land \|f\| = 2))))$
84	83	3imp	$⊢ (f Walks (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))) \to ((((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to (f Walks (G) W \land \|f\| = 2))$
85	84	com12	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to ((f Walks (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))) \to (f Walks (G) W \land \|f\| = 2))$
86	85	exlimdv	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to (\exists p (f Walks (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))) \to (f Walks (G) W \land \|f\| = 2))$
87	42 86	impbid	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to ((f Walks (G) W \land \|f\| = 2) \leftrightarrow \exists p (f Walks (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))))$
88	87	exbidv	$⊢ (((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \land W = ⟨“ a b c ”⟩) \to (\exists f (f Walks (G) W \land \|f\| = 2) \leftrightarrow \exists f \exists p (f Walks (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2))))$
89	88	pm5.32da	$⊢ ((G \in UPGraph \land a \in V) \land (b \in V \land c \in V)) \to ((W = ⟨“ a b c ”⟩ \land \exists f (f Walks (G) W \land \|f\| = 2)) \leftrightarrow (W = ⟨“ a b c ”⟩ \land \exists f \exists p (f Walks (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))))$
90	89	2rexbidva	$⊢ (G \in UPGraph \land a \in V) \to (\exists b \in V \exists c \in V (W = ⟨“ a b c ”⟩ \land \exists f (f Walks (G) W \land \|f\| = 2)) \leftrightarrow \exists b \in V \exists c \in V (W = ⟨“ a b c ”⟩ \land \exists f \exists p (f Walks (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))))$
91	7 90	syl5bb	$⊢ (G \in UPGraph \land a \in V) \to (\exists c \in V \exists b \in V (W = ⟨“ a b c ”⟩ \land \exists f (f Walks (G) W \land \|f\| = 2)) \leftrightarrow \exists b \in V \exists c \in V (W = ⟨“ a b c ”⟩ \land \exists f \exists p (f Walks (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))))$
92	91	rexbidva	$⊢ G \in UPGraph \to (\exists a \in V \exists c \in V \exists b \in V (W = ⟨“ a b c ”⟩ \land \exists f (f Walks (G) W \land \|f\| = 2)) \leftrightarrow \exists a \in V \exists b \in V \exists c \in V (W = ⟨“ a b c ”⟩ \land \exists f \exists p (f Walks (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))))$
93	3 6 92	3bitrd	$⊢ G \in UPGraph \to (W \in (2 WWalksN G) \leftrightarrow \exists a \in V \exists b \in V \exists c \in V (W = ⟨“ a b c ”⟩ \land \exists f \exists p (f Walks (G) p \land \|f\| = 2 \land (a = p (0) \land b = p (1) \land c = p (2)))))$

Metamath Proof Explorer

Theorem elwwlks2

Proof