Metamath Proof Explorer


Theorem 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 = ⟨“ ABCD ”⟩
3wlkd.f F = ⟨“ JKL ”⟩
3wlkd.s φ A V B V C V D V
3wlkd.n φ A B A C B C B D C D
3wlkd.e φ A B I J B C I K C D I L
3wlkd.v V = Vtx G
3wlkd.i I = iEdg G
3trld.n φ J K J L K L
3cycld.e φ A = D
Assertion 3cycld φ F Cycles G P

Proof

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