umgr2adedgwlk

Description: In a multigraph, two adjacent edges form a walk of length 2. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 29-Jan-2021)

	Ref	Expression
Hypotheses	umgr2adedgwlk.e	$⊢ E = Edg (G)$
	umgr2adedgwlk.i	$⊢ I = iEdg (G)$
	umgr2adedgwlk.f	$⊢ F = ⟨“ J K ”⟩$
	umgr2adedgwlk.p	$⊢ P = ⟨“ A B C ”⟩$
	umgr2adedgwlk.g	$⊢ φ \to G \in UMGraph$
	umgr2adedgwlk.a	$⊢ φ \to (\{A, B\} \in E \land \{B, C\} \in E)$
	umgr2adedgwlk.j	$⊢ φ \to I (J) = \{A, B\}$
	umgr2adedgwlk.k	$⊢ φ \to I (K) = \{B, C\}$
Assertion	umgr2adedgwlk	$⊢ φ \to (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		umgr2adedgwlk.e	$⊢ E = Edg (G)$
2		umgr2adedgwlk.i	$⊢ I = iEdg (G)$
3		umgr2adedgwlk.f	$⊢ F = ⟨“ J K ”⟩$
4		umgr2adedgwlk.p	$⊢ P = ⟨“ A B C ”⟩$
5		umgr2adedgwlk.g	$⊢ φ \to G \in UMGraph$
6		umgr2adedgwlk.a	$⊢ φ \to (\{A, B\} \in E \land \{B, C\} \in E)$
7		umgr2adedgwlk.j	$⊢ φ \to I (J) = \{A, B\}$
8		umgr2adedgwlk.k	$⊢ φ \to I (K) = \{B, C\}$
9		3anass	$⊢ (G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E) \leftrightarrow (G \in UMGraph \land (\{A, B\} \in E \land \{B, C\} \in E))$
10	5 6 9	sylanbrc	$⊢ φ \to (G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E)$
11	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)))$
12	10 11	syl	$⊢ φ \to ((A \neq B \land B \neq C) \land (A \in Vtx (G) \land B \in Vtx (G) \land C \in Vtx (G)))$
13	12	simprd	$⊢ φ \to (A \in Vtx (G) \land B \in Vtx (G) \land C \in Vtx (G))$
14	12	simpld	$⊢ φ \to (A \neq B \land B \neq C)$
15		ssid	$⊢ \{A, B\} \subseteq \{A, B\}$
16	15 7	sseqtrrid	$⊢ φ \to \{A, B\} \subseteq I (J)$
17		ssid	$⊢ \{B, C\} \subseteq \{B, C\}$
18	17 8	sseqtrrid	$⊢ φ \to \{B, C\} \subseteq I (K)$
19	16 18	jca	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K))$
20		eqid	$⊢ Vtx (G) = Vtx (G)$
21	4 3 13 14 19 20 2	2wlkd	$⊢ φ \to F Walks (G) P$
22	3	fveq2i	$⊢ \|F\| = \|⟨“ J K ”⟩\|$
23		s2len	$⊢ \|⟨“ J K ”⟩\| = 2$
24	22 23	eqtri	$⊢ \|F\| = 2$
25	24	a1i	$⊢ φ \to \|F\| = 2$
26		s3fv0	$⊢ A \in Vtx (G) \to ⟨“ A B C ”⟩ (0) = A$
27		s3fv1	$⊢ B \in Vtx (G) \to ⟨“ A B C ”⟩ (1) = B$
28		s3fv2	$⊢ C \in Vtx (G) \to ⟨“ A B C ”⟩ (2) = C$
29	26 27 28	3anim123i	$⊢ (A \in Vtx (G) \land B \in Vtx (G) \land C \in Vtx (G)) \to (⟨“ A B C ”⟩ (0) = A \land ⟨“ A B C ”⟩ (1) = B \land ⟨“ A B C ”⟩ (2) = C)$
30	13 29	syl	$⊢ φ \to (⟨“ A B C ”⟩ (0) = A \land ⟨“ A B C ”⟩ (1) = B \land ⟨“ A B C ”⟩ (2) = C)$
31	4	fveq1i	$⊢ P (0) = ⟨“ A B C ”⟩ (0)$
32	31	eqeq2i	$⊢ A = P (0) \leftrightarrow A = ⟨“ A B C ”⟩ (0)$
33		eqcom	$⊢ A = ⟨“ A B C ”⟩ (0) \leftrightarrow ⟨“ A B C ”⟩ (0) = A$
34	32 33	bitri	$⊢ A = P (0) \leftrightarrow ⟨“ A B C ”⟩ (0) = A$
35	4	fveq1i	$⊢ P (1) = ⟨“ A B C ”⟩ (1)$
36	35	eqeq2i	$⊢ B = P (1) \leftrightarrow B = ⟨“ A B C ”⟩ (1)$
37		eqcom	$⊢ B = ⟨“ A B C ”⟩ (1) \leftrightarrow ⟨“ A B C ”⟩ (1) = B$
38	36 37	bitri	$⊢ B = P (1) \leftrightarrow ⟨“ A B C ”⟩ (1) = B$
39	4	fveq1i	$⊢ P (2) = ⟨“ A B C ”⟩ (2)$
40	39	eqeq2i	$⊢ C = P (2) \leftrightarrow C = ⟨“ A B C ”⟩ (2)$
41		eqcom	$⊢ C = ⟨“ A B C ”⟩ (2) \leftrightarrow ⟨“ A B C ”⟩ (2) = C$
42	40 41	bitri	$⊢ C = P (2) \leftrightarrow ⟨“ A B C ”⟩ (2) = C$
43	34 38 42	3anbi123i	$⊢ (A = P (0) \land B = P (1) \land C = P (2)) \leftrightarrow (⟨“ A B C ”⟩ (0) = A \land ⟨“ A B C ”⟩ (1) = B \land ⟨“ A B C ”⟩ (2) = C)$
44	30 43	sylibr	$⊢ φ \to (A = P (0) \land B = P (1) \land C = P (2))$
45	21 25 44	3jca	$⊢ φ \to (F Walks (G) P \land \|F\| = 2 \land (A = P (0) \land B = P (1) \land C = P (2)))$

Metamath Proof Explorer

Theorem umgr2adedgwlk

Proof