umgr2wlkon

Description: For each pair of adjacent edges in a multigraph, there is a walk of length 2 between the not common vertices of the edges. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 30-Jan-2021)

		Ref	Expression
	Hypothesis	umgr2wlk.e	$⊢ E = Edg (G)$
	Assertion	umgr2wlkon	$⊢ (G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \to \exists f \exists p f (A WalksOn (G) C) p$

Proof

Step	Hyp	Ref	Expression
1		umgr2wlk.e	$⊢ E = Edg (G)$
2	1	umgr2wlk	$⊢ (G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \to \exists f \exists p (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2)))$
3		simp1	$⊢ (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2))) \to f Walks (G) p$
4		eqcom	$⊢ A = p (0) \leftrightarrow p (0) = A$
5	4	biimpi	$⊢ A = p (0) \to p (0) = A$
6	5	3ad2ant1	$⊢ (A = p (0) \land B = p (1) \land C = p (2)) \to p (0) = A$
7	6	3ad2ant3	$⊢ (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2))) \to p (0) = A$
8		fveq2	$⊢ 2 = \|f\| \to p (2) = p (\|f\|)$
9	8	eqcoms	$⊢ \|f\| = 2 \to p (2) = p (\|f\|)$
10	9	eqeq1d	$⊢ \|f\| = 2 \to (p (2) = C \leftrightarrow p (\|f\|) = C)$
11	10	biimpcd	$⊢ p (2) = C \to (\|f\| = 2 \to p (\|f\|) = C)$
12	11	eqcoms	$⊢ C = p (2) \to (\|f\| = 2 \to p (\|f\|) = C)$
13	12	3ad2ant3	$⊢ (A = p (0) \land B = p (1) \land C = p (2)) \to (\|f\| = 2 \to p (\|f\|) = C)$
14	13	com12	$⊢ \|f\| = 2 \to ((A = p (0) \land B = p (1) \land C = p (2)) \to p (\|f\|) = C)$
15	14	a1i	$⊢ f Walks (G) p \to (\|f\| = 2 \to ((A = p (0) \land B = p (1) \land C = p (2)) \to p (\|f\|) = C))$
16	15	3imp	$⊢ (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2))) \to p (\|f\|) = C$
17	3 7 16	3jca	$⊢ (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2))) \to (f Walks (G) p \land p (0) = A \land p (\|f\|) = C)$
18	17	adantl	$⊢ ((G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \land (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2)))) \to (f Walks (G) p \land p (0) = A \land p (\|f\|) = C)$
19	1	umgr2adedgwlklem	$⊢ (G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \to ((A \neq B \land B \neq C) \land (A \in Vtx (G) \land B \in Vtx (G) \land C \in Vtx (G)))$
20		simprr1	$⊢ ((G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \land ((A \neq B \land B \neq C) \land (A \in Vtx (G) \land B \in Vtx (G) \land C \in Vtx (G)))) \to A \in Vtx (G)$
21		simprr3	$⊢ ((G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \land ((A \neq B \land B \neq C) \land (A \in Vtx (G) \land B \in Vtx (G) \land C \in Vtx (G)))) \to C \in Vtx (G)$
22	20 21	jca	$⊢ ((G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \land ((A \neq B \land B \neq C) \land (A \in Vtx (G) \land B \in Vtx (G) \land C \in Vtx (G)))) \to (A \in Vtx (G) \land C \in Vtx (G))$
23	19 22	mpdan	$⊢ (G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \to (A \in Vtx (G) \land C \in Vtx (G))$
24		vex	$⊢ f \in V$
25		vex	$⊢ p \in V$
26	24 25	pm3.2i	$⊢ (f \in V \land p \in V)$
27	26	a1i	$⊢ ((G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \land (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2)))) \to (f \in V \land p \in V)$
28		eqid	$⊢ Vtx (G) = Vtx (G)$
29	28	iswlkon	$⊢ ((A \in Vtx (G) \land C \in Vtx (G)) \land (f \in V \land p \in V)) \to (f (A WalksOn (G) C) p \leftrightarrow (f Walks (G) p \land p (0) = A \land p (\|f\|) = C))$
30	23 27 29	syl2an2r	$⊢ ((G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \land (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2)))) \to (f (A WalksOn (G) C) p \leftrightarrow (f Walks (G) p \land p (0) = A \land p (\|f\|) = C))$
31	18 30	mpbird	$⊢ ((G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \land (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2)))) \to f (A WalksOn (G) C) p$
32	31	ex	$⊢ (G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \to ((f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2))) \to f (A WalksOn (G) C) p)$
33	32	2eximdv	$⊢ (G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \to (\exists f \exists p (f Walks (G) p \land \|f\| = 2 \land (A = p (0) \land B = p (1) \land C = p (2))) \to \exists f \exists p f (A WalksOn (G) C) p)$
34	2 33	mpd	$⊢ (G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \to \exists f \exists p f (A WalksOn (G) C) p$

Metamath Proof Explorer

Theorem umgr2wlkon

Proof