3cyclpd

Description: Construction of a 3-cycle from three given edges in a graph, containing an endpoint of one of these edges. (Contributed by Alexander van der Vekens, 17-Nov-2017) (Revised by AV, 10-Feb-2021) (Revised by AV, 24-Mar-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	3cyclpd	$⊢ φ \to (F Cycles (G) P \land \|F\| = 3 \land P (0) = A)$

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 9	3cycld	$⊢ φ \to F Cycles (G) P$
11	2	fveq2i	$⊢ \|F\| = \|⟨“ J K L ”⟩\|$
12		s3len	$⊢ \|⟨“ J K L ”⟩\| = 3$
13	11 12	eqtri	$⊢ \|F\| = 3$
14	13	a1i	$⊢ φ \to \|F\| = 3$
15	1	fveq1i	$⊢ P (0) = ⟨“ A B C D ”⟩ (0)$
16		s4fv0	$⊢ A \in V \to ⟨“ A B C D ”⟩ (0) = A$
17	15 16	syl5eq	$⊢ A \in V \to P (0) = A$
18	17	ad2antrr	$⊢ ((A \in V \land B \in V) \land (C \in V \land D \in V)) \to P (0) = A$
19	3 18	syl	$⊢ φ \to P (0) = A$
20	10 14 19	3jca	$⊢ φ \to (F Cycles (G) P \land \|F\| = 3 \land P (0) = A)$

Metamath Proof Explorer

Theorem 3cyclpd

Proof