3cycld

Description: Construction of a 3-cycle from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017) (Revised by AV, 10-Feb-2021) (Revised by AV, 24-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Hypotheses	3wlkd.p	$⊢ P = ⟨“ A B C D ”⟩$
	3wlkd.f	$⊢ F = ⟨“ J K L ”⟩$
	3wlkd.s	$⊢ φ \to ((A \in V \land B \in V) \land (C \in V \land D \in V))$
	3wlkd.n	$⊢ φ \to ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)$
	3wlkd.e	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K) \land \{C, D\} \subseteq I (L))$
	3wlkd.v	$⊢ V = Vtx (G)$
	3wlkd.i	$⊢ I = iEdg (G)$
	3trld.n	$⊢ φ \to (J \neq K \land J \neq L \land K \neq L)$
	3cycld.e	$⊢ φ \to A = D$
Assertion	3cycld	$⊢ φ \to F Cycles (G) P$

Proof

Step	Hyp	Ref	Expression
1		3wlkd.p	$⊢ P = ⟨“ A B C D ”⟩$
2		3wlkd.f	$⊢ F = ⟨“ J K L ”⟩$
3		3wlkd.s	$⊢ φ \to ((A \in V \land B \in V) \land (C \in V \land D \in V))$
4		3wlkd.n	$⊢ φ \to ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)$
5		3wlkd.e	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K) \land \{C, D\} \subseteq I (L))$
6		3wlkd.v	$⊢ V = Vtx (G)$
7		3wlkd.i	$⊢ I = iEdg (G)$
8		3trld.n	$⊢ φ \to (J \neq K \land J \neq L \land K \neq L)$
9		3cycld.e	$⊢ φ \to A = D$
10	1 2 3 4 5 6 7 8	3pthd	$⊢ φ \to F Paths (G) P$
11	1	fveq1i	$⊢ P (0) = ⟨“ A B C D ”⟩ (0)$
12		s4fv0	$⊢ A \in V \to ⟨“ A B C D ”⟩ (0) = A$
13	11 12	eqtrid	$⊢ A \in V \to P (0) = A$
14	13	ad3antrrr	$⊢ (((A \in V \land B \in V) \land (C \in V \land D \in V)) \land A = D) \to P (0) = A$
15		simpr	$⊢ (((A \in V \land B \in V) \land (C \in V \land D \in V)) \land A = D) \to A = D$
16	2	fveq2i	$⊢ \|F\| = \|⟨“ J K L ”⟩\|$
17		s3len	$⊢ \|⟨“ J K L ”⟩\| = 3$
18	16 17	eqtri	$⊢ \|F\| = 3$
19	1 18	fveq12i	$⊢ P (\|F\|) = ⟨“ A B C D ”⟩ (3)$
20		s4fv3	$⊢ D \in V \to ⟨“ A B C D ”⟩ (3) = D$
21	19 20	eqtr2id	$⊢ D \in V \to D = P (\|F\|)$
22	21	adantl	$⊢ (C \in V \land D \in V) \to D = P (\|F\|)$
23	22	ad2antlr	$⊢ (((A \in V \land B \in V) \land (C \in V \land D \in V)) \land A = D) \to D = P (\|F\|)$
24	14 15 23	3eqtrd	$⊢ (((A \in V \land B \in V) \land (C \in V \land D \in V)) \land A = D) \to P (0) = P (\|F\|)$
25	3 9 24	syl2anc	$⊢ φ \to P (0) = P (\|F\|)$
26		iscycl	$⊢ F Cycles (G) P \leftrightarrow (F Paths (G) P \land P (0) = P (\|F\|))$
27	10 25 26	sylanbrc	$⊢ φ \to F Cycles (G) P$

Metamath Proof Explorer

Theorem 3cycld

Proof