Metamath Proof Explorer

Theorem cycl3grtrilem

Description: Lemma for cycl3grtri . (Contributed by AV, 5-Oct-2025)

Ref Expression
Assertion cycl3grtrilem ⊢ G ∈ UPGraph ∧ F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F ∧ F = 3 → P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G

Proof

Step Hyp Ref Expression
1 pthiswlk ⊢ F Paths ⁡ G P → F Walks ⁡ G P
2 eqid ⊢ Edg ⁡ G = Edg ⁡ G
3 2 upgrwlkvtxedg ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P → ∀ x ∈ 0 ..^ F P ⁡ x P ⁡ x + 1 ∈ Edg ⁡ G
4 1 3 sylan2 ⊢ G ∈ UPGraph ∧ F Paths ⁡ G P → ∀ x ∈ 0 ..^ F P ⁡ x P ⁡ x + 1 ∈ Edg ⁡ G
5 4 adantr ⊢ G ∈ UPGraph ∧ F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F ∧ F = 3 → ∀ x ∈ 0 ..^ F P ⁡ x P ⁡ x + 1 ∈ Edg ⁡ G
6 oveq2 ⊢ F = 3 → 0 ..^ F = 0 ..^ 3
7 fzo0to3tp ⊢ 0 ..^ 3 = 0 1 2
8 6 7 eqtrdi ⊢ F = 3 → 0 ..^ F = 0 1 2
9 8 adantl ⊢ P ⁡ 0 = P ⁡ F ∧ F = 3 → 0 ..^ F = 0 1 2
10 9 adantl ⊢ G ∈ UPGraph ∧ F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F ∧ F = 3 → 0 ..^ F = 0 1 2
11 10 raleqdv ⊢ G ∈ UPGraph ∧ F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F ∧ F = 3 → ∀ x ∈ 0 ..^ F P ⁡ x P ⁡ x + 1 ∈ Edg ⁡ G ↔ ∀ x ∈ 0 1 2 P ⁡ x P ⁡ x + 1 ∈ Edg ⁡ G
12 fveq2 ⊢ F = 3 → P ⁡ F = P ⁡ 3
13 12 eqeq2d ⊢ F = 3 → P ⁡ 0 = P ⁡ F ↔ P ⁡ 0 = P ⁡ 3
14 c0ex ⊢ 0 ∈ V
15 1ex ⊢ 1 ∈ V
16 2ex ⊢ 2 ∈ V
17 fveq2 ⊢ x = 0 → P ⁡ x = P ⁡ 0
18 fv0p1e1 ⊢ x = 0 → P ⁡ x + 1 = P ⁡ 1
19 17 18 preq12d ⊢ x = 0 → P ⁡ x P ⁡ x + 1 = P ⁡ 0 P ⁡ 1
20 19 eleq1d ⊢ x = 0 → P ⁡ x P ⁡ x + 1 ∈ Edg ⁡ G ↔ P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G
21 fveq2 ⊢ x = 1 → P ⁡ x = P ⁡ 1
22 oveq1 ⊢ x = 1 → x + 1 = 1 + 1
23 1p1e2 ⊢ 1 + 1 = 2
24 22 23 eqtrdi ⊢ x = 1 → x + 1 = 2
25 24 fveq2d ⊢ x = 1 → P ⁡ x + 1 = P ⁡ 2
26 21 25 preq12d ⊢ x = 1 → P ⁡ x P ⁡ x + 1 = P ⁡ 1 P ⁡ 2
27 26 eleq1d ⊢ x = 1 → P ⁡ x P ⁡ x + 1 ∈ Edg ⁡ G ↔ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G
28 fveq2 ⊢ x = 2 → P ⁡ x = P ⁡ 2
29 oveq1 ⊢ x = 2 → x + 1 = 2 + 1
30 2p1e3 ⊢ 2 + 1 = 3
31 29 30 eqtrdi ⊢ x = 2 → x + 1 = 3
32 31 fveq2d ⊢ x = 2 → P ⁡ x + 1 = P ⁡ 3
33 28 32 preq12d ⊢ x = 2 → P ⁡ x P ⁡ x + 1 = P ⁡ 2 P ⁡ 3
34 33 eleq1d ⊢ x = 2 → P ⁡ x P ⁡ x + 1 ∈ Edg ⁡ G ↔ P ⁡ 2 P ⁡ 3 ∈ Edg ⁡ G
35 14 15 16 20 27 34 raltp ⊢ ∀ x ∈ 0 1 2 P ⁡ x P ⁡ x + 1 ∈ Edg ⁡ G ↔ P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 2 P ⁡ 3 ∈ Edg ⁡ G
36 simpr1 ⊢ P ⁡ 0 = P ⁡ 3 ∧ P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 2 P ⁡ 3 ∈ Edg ⁡ G → P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G
37 preq2 ⊢ P ⁡ 0 = P ⁡ 3 → P ⁡ 2 P ⁡ 0 = P ⁡ 2 P ⁡ 3
38 prcom ⊢ P ⁡ 2 P ⁡ 0 = P ⁡ 0 P ⁡ 2
39 37 38 eqtr3di ⊢ P ⁡ 0 = P ⁡ 3 → P ⁡ 2 P ⁡ 3 = P ⁡ 0 P ⁡ 2
40 39 eleq1d ⊢ P ⁡ 0 = P ⁡ 3 → P ⁡ 2 P ⁡ 3 ∈ Edg ⁡ G ↔ P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G
41 40 biimpcd ⊢ P ⁡ 2 P ⁡ 3 ∈ Edg ⁡ G → P ⁡ 0 = P ⁡ 3 → P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G
42 41 3ad2ant3 ⊢ P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 2 P ⁡ 3 ∈ Edg ⁡ G → P ⁡ 0 = P ⁡ 3 → P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G
43 42 impcom ⊢ P ⁡ 0 = P ⁡ 3 ∧ P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 2 P ⁡ 3 ∈ Edg ⁡ G → P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G
44 simpr2 ⊢ P ⁡ 0 = P ⁡ 3 ∧ P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 2 P ⁡ 3 ∈ Edg ⁡ G → P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G
45 36 43 44 3jca ⊢ P ⁡ 0 = P ⁡ 3 ∧ P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 2 P ⁡ 3 ∈ Edg ⁡ G → P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G
46 45 ex ⊢ P ⁡ 0 = P ⁡ 3 → P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 2 P ⁡ 3 ∈ Edg ⁡ G → P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G
47 35 46 biimtrid ⊢ P ⁡ 0 = P ⁡ 3 → ∀ x ∈ 0 1 2 P ⁡ x P ⁡ x + 1 ∈ Edg ⁡ G → P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G
48 13 47 biimtrdi ⊢ F = 3 → P ⁡ 0 = P ⁡ F → ∀ x ∈ 0 1 2 P ⁡ x P ⁡ x + 1 ∈ Edg ⁡ G → P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G
49 48 impcom ⊢ P ⁡ 0 = P ⁡ F ∧ F = 3 → ∀ x ∈ 0 1 2 P ⁡ x P ⁡ x + 1 ∈ Edg ⁡ G → P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G
50 49 adantl ⊢ G ∈ UPGraph ∧ F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F ∧ F = 3 → ∀ x ∈ 0 1 2 P ⁡ x P ⁡ x + 1 ∈ Edg ⁡ G → P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G
51 11 50 sylbid ⊢ G ∈ UPGraph ∧ F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F ∧ F = 3 → ∀ x ∈ 0 ..^ F P ⁡ x P ⁡ x + 1 ∈ Edg ⁡ G → P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G
52 5 51 mpd ⊢ G ∈ UPGraph ∧ F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F ∧ F = 3 → P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G