Metamath Proof Explorer


Theorem 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 = ⟨“ 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 3cyclpd φ F Cycles G P F = 3 P 0 = A

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 9 3cycld φ F Cycles G P
11 2 fveq2i F = ⟨“ JKL ”⟩
12 s3len ⟨“ JKL ”⟩ = 3
13 11 12 eqtri F = 3
14 13 a1i φ F = 3
15 1 fveq1i P 0 = ⟨“ ABCD ”⟩ 0
16 s4fv0 A V ⟨“ ABCD ”⟩ 0 = A
17 15 16 syl5eq A V P 0 = A
18 17 ad2antrr A V B V C V D V P 0 = A
19 3 18 syl φ P 0 = A
20 10 14 19 3jca φ F Cycles G P F = 3 P 0 = A