2cycld

Description: Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023)

	Ref	Expression
Hypotheses	2cycld.1	$⊢ P = ⟨“ A B C ”⟩$
	2cycld.2	$⊢ F = ⟨“ J K ”⟩$
	2cycld.3	$⊢ φ \to (A \in V \land B \in V \land C \in V)$
	2cycld.4	$⊢ φ \to (A \neq B \land B \neq C)$
	2cycld.5	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K))$
	2cycld.6	$⊢ V = Vtx (G)$
	2cycld.7	$⊢ I = iEdg (G)$
	2cycld.8	$⊢ φ \to J \neq K$
	2cycld.9	$⊢ φ \to A = C$
Assertion	2cycld	$⊢ φ \to F Cycles (G) P$

Step	Hyp	Ref	Expression
1		2cycld.1	$⊢ P = ⟨“ A B C ”⟩$
2		2cycld.2	$⊢ F = ⟨“ J K ”⟩$
3		2cycld.3	$⊢ φ \to (A \in V \land B \in V \land C \in V)$
4		2cycld.4	$⊢ φ \to (A \neq B \land B \neq C)$
5		2cycld.5	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K))$
6		2cycld.6	$⊢ V = Vtx (G)$
7		2cycld.7	$⊢ I = iEdg (G)$
8		2cycld.8	$⊢ φ \to J \neq K$
9		2cycld.9	$⊢ φ \to A = C$
10	1 2 3 4 5 6 7 8	2pthd	$⊢ φ \to F Paths (G) P$
11	1	fveq1i	$⊢ P (0) = ⟨“ A B C ”⟩ (0)$
12		s3fv0	$⊢ A \in V \to ⟨“ A B C ”⟩ (0) = A$
13	11 12	eqtrid	$⊢ A \in V \to P (0) = A$
14	13	3ad2ant1	$⊢ (A \in V \land B \in V \land C \in V) \to P (0) = A$
15	14	adantr	$⊢ ((A \in V \land B \in V \land C \in V) \land A = C) \to P (0) = A$
16		simpr	$⊢ ((A \in V \land B \in V \land C \in V) \land A = C) \to A = C$
17	2	fveq2i	$⊢ \|F\| = \|⟨“ J K ”⟩\|$
18		s2len	$⊢ \|⟨“ J K ”⟩\| = 2$
19	17 18	eqtri	$⊢ \|F\| = 2$
20	1 19	fveq12i	$⊢ P (\|F\|) = ⟨“ A B C ”⟩ (2)$
21		s3fv2	$⊢ C \in V \to ⟨“ A B C ”⟩ (2) = C$
22	20 21	eqtr2id	$⊢ C \in V \to C = P (\|F\|)$
23	22	3ad2ant3	$⊢ (A \in V \land B \in V \land C \in V) \to C = P (\|F\|)$
24	23	adantr	$⊢ ((A \in V \land B \in V \land C \in V) \land A = C) \to C = P (\|F\|)$
25	15 16 24	3eqtrd	$⊢ ((A \in V \land B \in V \land C \in V) \land A = C) \to P (0) = P (\|F\|)$
26	3 9 25	syl2anc	$⊢ φ \to P (0) = P (\|F\|)$
27		iscycl	$⊢ F Cycles (G) P \leftrightarrow (F Paths (G) P \land P (0) = P (\|F\|))$
28	10 26 27	sylanbrc	$⊢ φ \to F Cycles (G) P$

Metamath Proof Explorer