umgr2adedgspth

Description: In a multigraph, two adjacent edges with different endvertices form a simple path of length 2. (Contributed by Alexander van der Vekens, 1-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\}$
	umgr2adedgspth.n	$⊢ φ \to A \neq C$
Assertion	umgr2adedgspth	$⊢ φ \to F SPaths (G) P$

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		umgr2adedgspth.n	$⊢ φ \to A \neq C$
10		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))$
11	5 6 10	sylanbrc	$⊢ φ \to (G \in UMGraph \land \{A, B\} \in E \land \{B, C\} \in E)$
12	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)))$
13	11 12	syl	$⊢ φ \to ((A \neq B \land B \neq C) \land (A \in Vtx (G) \land B \in Vtx (G) \land C \in Vtx (G)))$
14	13	simprd	$⊢ φ \to (A \in Vtx (G) \land B \in Vtx (G) \land C \in Vtx (G))$
15	13	simpld	$⊢ φ \to (A \neq B \land B \neq C)$
16		ssid	$⊢ \{A, B\} \subseteq \{A, B\}$
17	16 7	sseqtrrid	$⊢ φ \to \{A, B\} \subseteq I (J)$
18		ssid	$⊢ \{B, C\} \subseteq \{B, C\}$
19	18 8	sseqtrrid	$⊢ φ \to \{B, C\} \subseteq I (K)$
20	17 19	jca	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K))$
21		eqid	$⊢ Vtx (G) = Vtx (G)$
22		fveq2	$⊢ K = J \to I (K) = I (J)$
23	22	eqcoms	$⊢ J = K \to I (K) = I (J)$
24	23	eqeq1d	$⊢ J = K \to (I (K) = \{B, C\} \leftrightarrow I (J) = \{B, C\})$
25		eqtr2	$⊢ (I (J) = \{B, C\} \land I (J) = \{A, B\}) \to \{B, C\} = \{A, B\}$
26	25	ex	$⊢ I (J) = \{B, C\} \to (I (J) = \{A, B\} \to \{B, C\} = \{A, B\})$
27	24 26	syl6bi	$⊢ J = K \to (I (K) = \{B, C\} \to (I (J) = \{A, B\} \to \{B, C\} = \{A, B\}))$
28	27	com13	$⊢ I (J) = \{A, B\} \to (I (K) = \{B, C\} \to (J = K \to \{B, C\} = \{A, B\}))$
29	7 8 28	sylc	$⊢ φ \to (J = K \to \{B, C\} = \{A, B\})$
30		eqcom	$⊢ \{B, C\} = \{A, B\} \leftrightarrow \{A, B\} = \{B, C\}$
31		prcom	$⊢ \{B, C\} = \{C, B\}$
32	31	eqeq2i	$⊢ \{A, B\} = \{B, C\} \leftrightarrow \{A, B\} = \{C, B\}$
33	30 32	bitri	$⊢ \{B, C\} = \{A, B\} \leftrightarrow \{A, B\} = \{C, B\}$
34	21 1	umgrpredgv	$⊢ (G \in UMGraph \land \{A, B\} \in E) \to (A \in Vtx (G) \land B \in Vtx (G))$
35	34	simpld	$⊢ (G \in UMGraph \land \{A, B\} \in E) \to A \in Vtx (G)$
36	35	ex	$⊢ G \in UMGraph \to (\{A, B\} \in E \to A \in Vtx (G))$
37	21 1	umgrpredgv	$⊢ (G \in UMGraph \land \{B, C\} \in E) \to (B \in Vtx (G) \land C \in Vtx (G))$
38	37	simprd	$⊢ (G \in UMGraph \land \{B, C\} \in E) \to C \in Vtx (G)$
39	38	ex	$⊢ G \in UMGraph \to (\{B, C\} \in E \to C \in Vtx (G))$
40	36 39	anim12d	$⊢ G \in UMGraph \to ((\{A, B\} \in E \land \{B, C\} \in E) \to (A \in Vtx (G) \land C \in Vtx (G)))$
41	5 6 40	sylc	$⊢ φ \to (A \in Vtx (G) \land C \in Vtx (G))$
42		preqr1g	$⊢ (A \in Vtx (G) \land C \in Vtx (G)) \to (\{A, B\} = \{C, B\} \to A = C)$
43	41 42	syl	$⊢ φ \to (\{A, B\} = \{C, B\} \to A = C)$
44		eqneqall	$⊢ A = C \to (A \neq C \to J \neq K)$
45	43 9 44	syl6ci	$⊢ φ \to (\{A, B\} = \{C, B\} \to J \neq K)$
46	33 45	biimtrid	$⊢ φ \to (\{B, C\} = \{A, B\} \to J \neq K)$
47	29 46	syld	$⊢ φ \to (J = K \to J \neq K)$
48		neqne	$⊢ \neg J = K \to J \neq K$
49	47 48	pm2.61d1	$⊢ φ \to J \neq K$
50	4 3 14 15 20 21 2 49 9	2spthd	$⊢ φ \to F SPaths (G) P$

Metamath Proof Explorer

Theorem umgr2adedgspth

Proof