Metamath Proof Explorer


Theorem 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 = ⟨“ ABC ”⟩
2cycld.2 F = ⟨“ JK ”⟩
2cycld.3 φ A V B V C V
2cycld.4 φ A B B C
2cycld.5 φ A B I J B C I K
2cycld.6 V = Vtx G
2cycld.7 I = iEdg G
2cycld.8 φ J K
2cycld.9 φ A = C
Assertion 2cycld φ F Cycles G P

Proof

Step Hyp Ref Expression
1 2cycld.1 P = ⟨“ ABC ”⟩
2 2cycld.2 F = ⟨“ JK ”⟩
3 2cycld.3 φ A V B V C V
4 2cycld.4 φ A B B C
5 2cycld.5 φ A B I J B C I K
6 2cycld.6 V = Vtx G
7 2cycld.7 I = iEdg G
8 2cycld.8 φ J K
9 2cycld.9 φ A = C
10 1 2 3 4 5 6 7 8 2pthd φ F Paths G P
11 1 fveq1i P 0 = ⟨“ ABC ”⟩ 0
12 s3fv0 A V ⟨“ ABC ”⟩ 0 = A
13 11 12 syl5eq A V P 0 = A
14 13 3ad2ant1 A V B V C V P 0 = A
15 14 adantr A V B V C V A = C P 0 = A
16 simpr A V B V C V A = C A = C
17 2 fveq2i F = ⟨“ JK ”⟩
18 s2len ⟨“ JK ”⟩ = 2
19 17 18 eqtri F = 2
20 1 19 fveq12i P F = ⟨“ ABC ”⟩ 2
21 s3fv2 C V ⟨“ ABC ”⟩ 2 = C
22 20 21 eqtr2id C V C = P F
23 22 3ad2ant3 A V B V C V C = P F
24 23 adantr A V B V C V A = C C = P F
25 15 16 24 3eqtrd A V B V C V A = C P 0 = P F
26 3 9 25 syl2anc φ P 0 = P F
27 iscycl F Cycles G P F Paths G P P 0 = P F
28 10 26 27 sylanbrc φ F Cycles G P