wpthswwlks2on

Description: For two different vertices, a walk of length 2 between these vertices is a simple path of length 2 between these vertices in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018) (Revised by AV, 16-Mar-2022) (Revised by Ender Ting, 29-Jan-2026)

		Ref	Expression
	Assertion	wpthswwlks2on	$⊢ (G \in USGraph \land A \neq B) \to A (2 WSPathsNOn G) B = A (2 WWalksNOn G) B$

Proof

Step	Hyp	Ref	Expression
1		wwlknon	$⊢ w \in (A (2 WWalksNOn G) B) \leftrightarrow (w \in (2 WWalksN G) \land w (0) = A \land w (2) = B)$
2	1	a1i	$⊢ (G \in USGraph \land A \neq B) \to (w \in (A (2 WWalksNOn G) B) \leftrightarrow (w \in (2 WWalksN G) \land w (0) = A \land w (2) = B))$
3	2	anbi1d	$⊢ (G \in USGraph \land A \neq B) \to ((w \in (A (2 WWalksNOn G) B) \land \exists f f (A SPathsOn (G) B) w) \leftrightarrow ((w \in (2 WWalksN G) \land w (0) = A \land w (2) = B) \land \exists f f (A SPathsOn (G) B) w))$
4		3anass	$⊢ (w \in (2 WWalksN G) \land w (0) = A \land w (2) = B) \leftrightarrow (w \in (2 WWalksN G) \land (w (0) = A \land w (2) = B))$
5	4	anbi1i	$⊢ ((w \in (2 WWalksN G) \land w (0) = A \land w (2) = B) \land \exists f f (A SPathsOn (G) B) w) \leftrightarrow ((w \in (2 WWalksN G) \land (w (0) = A \land w (2) = B)) \land \exists f f (A SPathsOn (G) B) w)$
6		anass	$⊢ ((w \in (2 WWalksN G) \land (w (0) = A \land w (2) = B)) \land \exists f f (A SPathsOn (G) B) w) \leftrightarrow (w \in (2 WWalksN G) \land ((w (0) = A \land w (2) = B) \land \exists f f (A SPathsOn (G) B) w))$
7	5 6	bitri	$⊢ ((w \in (2 WWalksN G) \land w (0) = A \land w (2) = B) \land \exists f f (A SPathsOn (G) B) w) \leftrightarrow (w \in (2 WWalksN G) \land ((w (0) = A \land w (2) = B) \land \exists f f (A SPathsOn (G) B) w))$
8	3 7	bitrdi	$⊢ (G \in USGraph \land A \neq B) \to ((w \in (A (2 WWalksNOn G) B) \land \exists f f (A SPathsOn (G) B) w) \leftrightarrow (w \in (2 WWalksN G) \land ((w (0) = A \land w (2) = B) \land \exists f f (A SPathsOn (G) B) w)))$
9	8	rabbidva2	$⊢ (G \in USGraph \land A \neq B) \to \{w \in (A (2 WWalksNOn G) B) \| \exists f f (A SPathsOn (G) B) w\} = \{w \in (2 WWalksN G) \| ((w (0) = A \land w (2) = B) \land \exists f f (A SPathsOn (G) B) w)\}$
10		usgruspgr	$⊢ G \in USGraph \to G \in USHGraph$
11		wlklnwwlkn	$⊢ G \in USHGraph \to (\exists f (f Walks (G) w \land \|f\| = 2) \leftrightarrow w \in (2 WWalksN G))$
12	10 11	syl	$⊢ G \in USGraph \to (\exists f (f Walks (G) w \land \|f\| = 2) \leftrightarrow w \in (2 WWalksN G))$
13	12	bicomd	$⊢ G \in USGraph \to (w \in (2 WWalksN G) \leftrightarrow \exists f (f Walks (G) w \land \|f\| = 2))$
14	13	adantr	$⊢ (G \in USGraph \land A \neq B) \to (w \in (2 WWalksN G) \leftrightarrow \exists f (f Walks (G) w \land \|f\| = 2))$
15		simprl	$⊢ (((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \land (f Walks (G) w \land \|f\| = 2)) \to f Walks (G) w$
16		simprl	$⊢ ((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \to w (0) = A$
17	16	adantr	$⊢ (((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \land (f Walks (G) w \land \|f\| = 2)) \to w (0) = A$
18		fveq2	$⊢ \|f\| = 2 \to w (\|f\|) = w (2)$
19	18	ad2antll	$⊢ (((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \land (f Walks (G) w \land \|f\| = 2)) \to w (\|f\|) = w (2)$
20		simprr	$⊢ ((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \to w (2) = B$
21	20	adantr	$⊢ (((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \land (f Walks (G) w \land \|f\| = 2)) \to w (2) = B$
22	19 21	eqtrd	$⊢ (((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \land (f Walks (G) w \land \|f\| = 2)) \to w (\|f\|) = B$
23		eqid	$⊢ Vtx (G) = Vtx (G)$
24	23	wlkp	$⊢ f Walks (G) w \to w : (0 \dots \|f\|) ⟶ Vtx (G)$
25		oveq2	$⊢ \|f\| = 2 \to (0 \dots \|f\|) = (0 \dots 2)$
26	25	feq2d	$⊢ \|f\| = 2 \to (w : (0 \dots \|f\|) ⟶ Vtx (G) \leftrightarrow w : (0 \dots 2) ⟶ Vtx (G))$
27	24 26	syl5ibcom	$⊢ f Walks (G) w \to (\|f\| = 2 \to w : (0 \dots 2) ⟶ Vtx (G))$
28	27	imp	$⊢ (f Walks (G) w \land \|f\| = 2) \to w : (0 \dots 2) ⟶ Vtx (G)$
29		id	$⊢ w : (0 \dots 2) ⟶ Vtx (G) \to w : (0 \dots 2) ⟶ Vtx (G)$
30		2nn0	$⊢ 2 \in ℕ_{0}$
31		0elfz	$⊢ 2 \in ℕ_{0} \to 0 \in (0 \dots 2)$
32	30 31	mp1i	$⊢ w : (0 \dots 2) ⟶ Vtx (G) \to 0 \in (0 \dots 2)$
33	29 32	ffvelcdmd	$⊢ w : (0 \dots 2) ⟶ Vtx (G) \to w (0) \in Vtx (G)$
34		nn0fz0	$⊢ 2 \in ℕ_{0} \leftrightarrow 2 \in (0 \dots 2)$
35	30 34	mpbi	$⊢ 2 \in (0 \dots 2)$
36	35	a1i	$⊢ w : (0 \dots 2) ⟶ Vtx (G) \to 2 \in (0 \dots 2)$
37	29 36	ffvelcdmd	$⊢ w : (0 \dots 2) ⟶ Vtx (G) \to w (2) \in Vtx (G)$
38	33 37	jca	$⊢ w : (0 \dots 2) ⟶ Vtx (G) \to (w (0) \in Vtx (G) \land w (2) \in Vtx (G))$
39	28 38	syl	$⊢ (f Walks (G) w \land \|f\| = 2) \to (w (0) \in Vtx (G) \land w (2) \in Vtx (G))$
40		eleq1	$⊢ w (0) = A \to (w (0) \in Vtx (G) \leftrightarrow A \in Vtx (G))$
41		eleq1	$⊢ w (2) = B \to (w (2) \in Vtx (G) \leftrightarrow B \in Vtx (G))$
42	40 41	bi2anan9	$⊢ (w (0) = A \land w (2) = B) \to ((w (0) \in Vtx (G) \land w (2) \in Vtx (G)) \leftrightarrow (A \in Vtx (G) \land B \in Vtx (G)))$
43	39 42	imbitrid	$⊢ (w (0) = A \land w (2) = B) \to ((f Walks (G) w \land \|f\| = 2) \to (A \in Vtx (G) \land B \in Vtx (G)))$
44	43	adantl	$⊢ ((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \to ((f Walks (G) w \land \|f\| = 2) \to (A \in Vtx (G) \land B \in Vtx (G)))$
45	44	imp	$⊢ (((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \land (f Walks (G) w \land \|f\| = 2)) \to (A \in Vtx (G) \land B \in Vtx (G))$
46		vex	$⊢ f \in V$
47		vex	$⊢ w \in V$
48	46 47	pm3.2i	$⊢ (f \in V \land w \in V)$
49	23	iswlkon	$⊢ ((A \in Vtx (G) \land B \in Vtx (G)) \land (f \in V \land w \in V)) \to (f (A WalksOn (G) B) w \leftrightarrow (f Walks (G) w \land w (0) = A \land w (\|f\|) = B))$
50	45 48 49	sylancl	$⊢ (((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \land (f Walks (G) w \land \|f\| = 2)) \to (f (A WalksOn (G) B) w \leftrightarrow (f Walks (G) w \land w (0) = A \land w (\|f\|) = B))$
51	15 17 22 50	mpbir3and	$⊢ (((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \land (f Walks (G) w \land \|f\| = 2)) \to f (A WalksOn (G) B) w$
52		simplll	$⊢ (((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \land (f Walks (G) w \land \|f\| = 2)) \to G \in USGraph$
53		simprr	$⊢ (((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \land (f Walks (G) w \land \|f\| = 2)) \to \|f\| = 2$
54		simpllr	$⊢ (((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \land (f Walks (G) w \land \|f\| = 2)) \to A \neq B$
55		usgr2wlkspth	$⊢ (G \in USGraph \land \|f\| = 2 \land A \neq B) \to (f (A WalksOn (G) B) w \leftrightarrow f (A SPathsOn (G) B) w)$
56	52 53 54 55	syl3anc	$⊢ (((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \land (f Walks (G) w \land \|f\| = 2)) \to (f (A WalksOn (G) B) w \leftrightarrow f (A SPathsOn (G) B) w)$
57	51 56	mpbid	$⊢ (((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \land (f Walks (G) w \land \|f\| = 2)) \to f (A SPathsOn (G) B) w$
58	57	ex	$⊢ ((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \to ((f Walks (G) w \land \|f\| = 2) \to f (A SPathsOn (G) B) w)$
59	58	eximdv	$⊢ ((G \in USGraph \land A \neq B) \land (w (0) = A \land w (2) = B)) \to (\exists f (f Walks (G) w \land \|f\| = 2) \to \exists f f (A SPathsOn (G) B) w)$
60	59	ex	$⊢ (G \in USGraph \land A \neq B) \to ((w (0) = A \land w (2) = B) \to (\exists f (f Walks (G) w \land \|f\| = 2) \to \exists f f (A SPathsOn (G) B) w))$
61	60	com23	$⊢ (G \in USGraph \land A \neq B) \to (\exists f (f Walks (G) w \land \|f\| = 2) \to ((w (0) = A \land w (2) = B) \to \exists f f (A SPathsOn (G) B) w))$
62	14 61	sylbid	$⊢ (G \in USGraph \land A \neq B) \to (w \in (2 WWalksN G) \to ((w (0) = A \land w (2) = B) \to \exists f f (A SPathsOn (G) B) w))$
63	62	imp	$⊢ ((G \in USGraph \land A \neq B) \land w \in (2 WWalksN G)) \to ((w (0) = A \land w (2) = B) \to \exists f f (A SPathsOn (G) B) w)$
64	63	pm4.71d	$⊢ ((G \in USGraph \land A \neq B) \land w \in (2 WWalksN G)) \to ((w (0) = A \land w (2) = B) \leftrightarrow ((w (0) = A \land w (2) = B) \land \exists f f (A SPathsOn (G) B) w))$
65	64	bicomd	$⊢ ((G \in USGraph \land A \neq B) \land w \in (2 WWalksN G)) \to (((w (0) = A \land w (2) = B) \land \exists f f (A SPathsOn (G) B) w) \leftrightarrow (w (0) = A \land w (2) = B))$
66	65	rabbidva	$⊢ (G \in USGraph \land A \neq B) \to \{w \in (2 WWalksN G) \| ((w (0) = A \land w (2) = B) \land \exists f f (A SPathsOn (G) B) w)\} = \{w \in (2 WWalksN G) \| (w (0) = A \land w (2) = B)\}$
67	9 66	eqtrd	$⊢ (G \in USGraph \land A \neq B) \to \{w \in (A (2 WWalksNOn G) B) \| \exists f f (A SPathsOn (G) B) w\} = \{w \in (2 WWalksN G) \| (w (0) = A \land w (2) = B)\}$
68	23	iswspthsnon	$⊢ A (2 WSPathsNOn G) B = \{w \in (A (2 WWalksNOn G) B) \| \exists f f (A SPathsOn (G) B) w\}$
69	23	iswwlksnon	$⊢ A (2 WWalksNOn G) B = \{w \in (2 WWalksN G) \| (w (0) = A \land w (2) = B)\}$
70	67 68 69	3eqtr4g	$⊢ (G \in USGraph \land A \neq B) \to A (2 WSPathsNOn G) B = A (2 WWalksNOn G) B$

Metamath Proof Explorer

Theorem wpthswwlks2on

Proof