Metamath Proof Explorer

Theorem grtriclwlk3

Description: A triangle induces a closed walk of length 3 . (Contributed by AV, 26-Jul-2025)

Ref Expression
Hypotheses grtriclwlk3.t No typesetting found for |- ( ph -> T e. ( GrTriangles ` G ) ) with typecode |-
grtriclwlk3.p ⊢ φ → P : 0 ..^ 3 ⟶ 1-1 onto T
Assertion grtriclwlk3 ⊢ φ → P ∈ 3 ClWWalksN G

Proof

Step Hyp Ref Expression
1 grtriclwlk3.t Could not format ( ph -> T e. ( GrTriangles ` G ) ) : No typesetting found for |- ( ph -> T e. ( GrTriangles ` G ) ) with typecode |-
2 grtriclwlk3.p ⊢ φ → P : 0 ..^ 3 ⟶ 1-1 onto T
3 f1ofn ⊢ P : 0 ..^ 3 ⟶ 1-1 onto T → P Fn 0 ..^ 3
4 hashfn ⊢ P Fn 0 ..^ 3 → P = 0 ..^ 3
5 2 3 4 3syl ⊢ φ → P = 0 ..^ 3
6 3nn0 ⊢ 3 ∈ ℕ 0
7 hashfzo0 ⊢ 3 ∈ ℕ 0 → 0 ..^ 3 = 3
8 6 7 mp1i ⊢ φ → 0 ..^ 3 = 3
9 5 8 eqtrd ⊢ φ → P = 3
10 f1of ⊢ P : 0 ..^ 3 ⟶ 1-1 onto T → P : 0 ..^ 3 ⟶ T
11 2 10 syl ⊢ φ → P : 0 ..^ 3 ⟶ T
12 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
13 12 grtrissvtx Could not format ( T e. ( GrTriangles ` G ) -> T C_ ( Vtx ` G ) ) : No typesetting found for |- ( T e. ( GrTriangles ` G ) -> T C_ ( Vtx ` G ) ) with typecode |-
14 1 13 syl ⊢ φ → T ⊆ Vtx ⁡ G
15 11 14 jca ⊢ φ → P : 0 ..^ 3 ⟶ T ∧ T ⊆ Vtx ⁡ G
16 15 adantr ⊢ φ ∧ P = 3 → P : 0 ..^ 3 ⟶ T ∧ T ⊆ Vtx ⁡ G
17 fss ⊢ P : 0 ..^ 3 ⟶ T ∧ T ⊆ Vtx ⁡ G → P : 0 ..^ 3 ⟶ Vtx ⁡ G
18 iswrdi ⊢ P : 0 ..^ 3 ⟶ Vtx ⁡ G → P ∈ Word Vtx ⁡ G
19 16 17 18 3syl ⊢ φ ∧ P = 3 → P ∈ Word Vtx ⁡ G
20 oveq1 ⊢ P = 3 → P − 1 = 3 − 1
21 3m1e2 ⊢ 3 − 1 = 2
22 20 21 eqtrdi ⊢ P = 3 → P − 1 = 2
23 22 oveq2d ⊢ P = 3 → 0 ..^ P − 1 = 0 ..^ 2
24 fzo0to2pr ⊢ 0 ..^ 2 = 0 1
25 23 24 eqtrdi ⊢ P = 3 → 0 ..^ P − 1 = 0 1
26 25 eleq2d ⊢ P = 3 → i ∈ 0 ..^ P − 1 ↔ i ∈ 0 1
27 26 adantl ⊢ φ ∧ P = 3 → i ∈ 0 ..^ P − 1 ↔ i ∈ 0 1
28 1 2 jca Could not format ( ph -> ( T e. ( GrTriangles ` G ) /\ P : ( 0 ..^ 3 ) -1-1-onto-> T ) ) : No typesetting found for |- ( ph -> ( T e. ( GrTriangles ` G ) /\ P : ( 0 ..^ 3 ) -1-1-onto-> T ) ) with typecode |-
29 eqid ⊢ Edg ⁡ G = Edg ⁡ G
30 12 29 grtrif1o Could not format ( ( T e. ( GrTriangles ` G ) /\ P : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 0 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) ) ) : No typesetting found for |- ( ( T e. ( GrTriangles ` G ) /\ P : ( 0 ..^ 3 ) -1-1-onto-> T ) -> ( { ( P ` 0 ) , ( P ` 1 ) } e. ( Edg ` G ) /\ { ( P ` 0 ) , ( P ` 2 ) } e. ( Edg ` G ) /\ { ( P ` 1 ) , ( P ` 2 ) } e. ( Edg ` G ) ) ) with typecode |-
31 simp1 ⊢ P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G → P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G
32 28 30 31 3syl ⊢ φ → P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G
33 32 adantr ⊢ φ ∧ P = 3 → P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G
34 fveq2 ⊢ i = 0 → P ⁡ i = P ⁡ 0
35 fv0p1e1 ⊢ i = 0 → P ⁡ i + 1 = P ⁡ 1
36 34 35 preq12d ⊢ i = 0 → P ⁡ i P ⁡ i + 1 = P ⁡ 0 P ⁡ 1
37 36 eleq1d ⊢ i = 0 → P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ↔ P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G
38 33 37 imbitrrid ⊢ i = 0 → φ ∧ P = 3 → P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G
39 simp3 ⊢ P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G → P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G
40 28 30 39 3syl ⊢ φ → P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G
41 40 adantr ⊢ φ ∧ P = 3 → P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G
42 fveq2 ⊢ i = 1 → P ⁡ i = P ⁡ 1
43 oveq1 ⊢ i = 1 → i + 1 = 1 + 1
44 1p1e2 ⊢ 1 + 1 = 2
45 43 44 eqtrdi ⊢ i = 1 → i + 1 = 2
46 45 fveq2d ⊢ i = 1 → P ⁡ i + 1 = P ⁡ 2
47 42 46 preq12d ⊢ i = 1 → P ⁡ i P ⁡ i + 1 = P ⁡ 1 P ⁡ 2
48 47 eleq1d ⊢ i = 1 → P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ↔ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G
49 41 48 imbitrrid ⊢ i = 1 → φ ∧ P = 3 → P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G
50 38 49 jaoi ⊢ i = 0 ∨ i = 1 → φ ∧ P = 3 → P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G
51 elpri ⊢ i ∈ 0 1 → i = 0 ∨ i = 1
52 50 51 syl11 ⊢ φ ∧ P = 3 → i ∈ 0 1 → P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G
53 27 52 sylbid ⊢ φ ∧ P = 3 → i ∈ 0 ..^ P − 1 → P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G
54 53 ralrimiv ⊢ φ ∧ P = 3 → ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G
55 ovexd ⊢ P : 0 ..^ 3 ⟶ 1-1 onto T → 0 ..^ 3 ∈ V
56 10 55 jca ⊢ P : 0 ..^ 3 ⟶ 1-1 onto T → P : 0 ..^ 3 ⟶ T ∧ 0 ..^ 3 ∈ V
57 fex ⊢ P : 0 ..^ 3 ⟶ T ∧ 0 ..^ 3 ∈ V → P ∈ V
58 2 56 57 3syl ⊢ φ → P ∈ V
59 58 adantr ⊢ φ ∧ P = 3 → P ∈ V
60 lsw ⊢ P ∈ V → lastS ⁡ P = P ⁡ P − 1
61 59 60 syl ⊢ φ ∧ P = 3 → lastS ⁡ P = P ⁡ P − 1
62 22 fveq2d ⊢ P = 3 → P ⁡ P − 1 = P ⁡ 2
63 62 adantl ⊢ φ ∧ P = 3 → P ⁡ P − 1 = P ⁡ 2
64 61 63 eqtrd ⊢ φ ∧ P = 3 → lastS ⁡ P = P ⁡ 2
65 64 preq1d ⊢ φ ∧ P = 3 → lastS ⁡ P P ⁡ 0 = P ⁡ 2 P ⁡ 0
66 prcom ⊢ P ⁡ 0 P ⁡ 2 = P ⁡ 2 P ⁡ 0
67 66 eleq1i ⊢ P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G ↔ P ⁡ 2 P ⁡ 0 ∈ Edg ⁡ G
68 67 biimpi ⊢ P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G → P ⁡ 2 P ⁡ 0 ∈ Edg ⁡ G
69 68 3ad2ant2 ⊢ P ⁡ 0 P ⁡ 1 ∈ Edg ⁡ G ∧ P ⁡ 0 P ⁡ 2 ∈ Edg ⁡ G ∧ P ⁡ 1 P ⁡ 2 ∈ Edg ⁡ G → P ⁡ 2 P ⁡ 0 ∈ Edg ⁡ G
70 28 30 69 3syl ⊢ φ → P ⁡ 2 P ⁡ 0 ∈ Edg ⁡ G
71 70 adantr ⊢ φ ∧ P = 3 → P ⁡ 2 P ⁡ 0 ∈ Edg ⁡ G
72 65 71 eqeltrd ⊢ φ ∧ P = 3 → lastS ⁡ P P ⁡ 0 ∈ Edg ⁡ G
73 19 54 72 3jca ⊢ φ ∧ P = 3 → P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ P P ⁡ 0 ∈ Edg ⁡ G
74 simpr ⊢ φ ∧ P = 3 → P = 3
75 73 74 jca ⊢ φ ∧ P = 3 → P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ P P ⁡ 0 ∈ Edg ⁡ G ∧ P = 3
76 9 75 mpdan ⊢ φ → P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ P P ⁡ 0 ∈ Edg ⁡ G ∧ P = 3
77 3nn ⊢ 3 ∈ ℕ
78 12 29 isclwwlknx ⊢ 3 ∈ ℕ → P ∈ 3 ClWWalksN G ↔ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ P P ⁡ 0 ∈ Edg ⁡ G ∧ P = 3
79 77 78 mp1i ⊢ φ → P ∈ 3 ClWWalksN G ↔ P ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ P − 1 P ⁡ i P ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ P P ⁡ 0 ∈ Edg ⁡ G ∧ P = 3
80 76 79 mpbird ⊢ φ → P ∈ 3 ClWWalksN G