Metamath Proof Explorer

Theorem iseqlg

Description: Property of a triangle being equilateral. (Contributed by Thierry Arnoux, 5-Oct-2020)

Ref Expression
Hypotheses iseqlg.p ⊢ P = Base G
iseqlg.m ⊢ - ˙ = dist ⁡ G
iseqlg.i ⊢ I = Itv ⁡ G
iseqlg.l ⊢ L = Line 𝒢 ⁡ G
iseqlg.g ⊢ φ → G ∈ 𝒢 Tarski
iseqlg.a ⊢ φ → A ∈ P
iseqlg.b ⊢ φ → B ∈ P
iseqlg.c ⊢ φ → C ∈ P
Assertion iseqlg ⊢ φ → ⟨“ ABC ”⟩ ∈ Equilaterals 𝒢 ⁡ G ↔ ⟨“ ABC ”⟩ ∼ 𝒢 ⁡ G ⟨“ BCA ”⟩

Proof

Step Hyp Ref Expression
1 iseqlg.p ⊢ P = Base G
2 iseqlg.m ⊢ - ˙ = dist ⁡ G
3 iseqlg.i ⊢ I = Itv ⁡ G
4 iseqlg.l ⊢ L = Line 𝒢 ⁡ G
5 iseqlg.g ⊢ φ → G ∈ 𝒢 Tarski
6 iseqlg.a ⊢ φ → A ∈ P
7 iseqlg.b ⊢ φ → B ∈ P
8 iseqlg.c ⊢ φ → C ∈ P
9 elex ⊢ G ∈ 𝒢 Tarski → G ∈ V
10 fveq2 ⊢ g = G → Base g = Base G
11 10 1 eqtr4di ⊢ g = G → Base g = P
12 11 oveq1d ⊢ g = G → Base g 0 ..^ 3 = P 0 ..^ 3
13 fveq2 ⊢ g = G → ∼ 𝒢 ⁡ g = ∼ 𝒢 ⁡ G
14 13 breqd ⊢ g = G → x ∼ 𝒢 ⁡ g ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩ ↔ x ∼ 𝒢 ⁡ G ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩
15 12 14 rabeqbidv ⊢ g = G → x ∈ Base g 0 ..^ 3 | x ∼ 𝒢 ⁡ g ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩ = x ∈ P 0 ..^ 3 | x ∼ 𝒢 ⁡ G ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩
16 df-eqlg ⊢ Equilaterals 𝒢 = g ∈ V ⟼ x ∈ Base g 0 ..^ 3 | x ∼ 𝒢 ⁡ g ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩
17 ovex ⊢ P 0 ..^ 3 ∈ V
18 17 rabex ⊢ x ∈ P 0 ..^ 3 | x ∼ 𝒢 ⁡ G ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩ ∈ V
19 15 16 18 fvmpt ⊢ G ∈ V → Equilaterals 𝒢 ⁡ G = x ∈ P 0 ..^ 3 | x ∼ 𝒢 ⁡ G ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩
20 5 9 19 3syl ⊢ φ → Equilaterals 𝒢 ⁡ G = x ∈ P 0 ..^ 3 | x ∼ 𝒢 ⁡ G ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩
21 20 eleq2d ⊢ φ → ⟨“ ABC ”⟩ ∈ Equilaterals 𝒢 ⁡ G ↔ ⟨“ ABC ”⟩ ∈ x ∈ P 0 ..^ 3 | x ∼ 𝒢 ⁡ G ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩
22 id ⊢ x = ⟨“ ABC ”⟩ → x = ⟨“ ABC ”⟩
23 fveq1 ⊢ x = ⟨“ ABC ”⟩ → x ⁡ 1 = ⟨“ ABC ”⟩ ⁡ 1
24 fveq1 ⊢ x = ⟨“ ABC ”⟩ → x ⁡ 2 = ⟨“ ABC ”⟩ ⁡ 2
25 fveq1 ⊢ x = ⟨“ ABC ”⟩ → x ⁡ 0 = ⟨“ ABC ”⟩ ⁡ 0
26 23 24 25 s3eqd ⊢ x = ⟨“ ABC ”⟩ → ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩ = ⟨“ ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ⟨“ ABC ”⟩ ⁡ 0 ”⟩
27 22 26 breq12d ⊢ x = ⟨“ ABC ”⟩ → x ∼ 𝒢 ⁡ G ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩ ↔ ⟨“ ABC ”⟩ ∼ 𝒢 ⁡ G ⟨“ ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ⟨“ ABC ”⟩ ⁡ 0 ”⟩
28 27 elrab ⊢ ⟨“ ABC ”⟩ ∈ x ∈ P 0 ..^ 3 | x ∼ 𝒢 ⁡ G ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩ ↔ ⟨“ ABC ”⟩ ∈ P 0 ..^ 3 ∧ ⟨“ ABC ”⟩ ∼ 𝒢 ⁡ G ⟨“ ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ⟨“ ABC ”⟩ ⁡ 0 ”⟩
29 28 a1i ⊢ φ → ⟨“ ABC ”⟩ ∈ x ∈ P 0 ..^ 3 | x ∼ 𝒢 ⁡ G ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩ ↔ ⟨“ ABC ”⟩ ∈ P 0 ..^ 3 ∧ ⟨“ ABC ”⟩ ∼ 𝒢 ⁡ G ⟨“ ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ⟨“ ABC ”⟩ ⁡ 0 ”⟩
30 6 7 8 s3cld ⊢ φ → ⟨“ ABC ”⟩ ∈ Word P
31 s3len ⊢ ⟨“ ABC ”⟩ = 3
32 1 fvexi ⊢ P ∈ V
33 3nn0 ⊢ 3 ∈ ℕ 0
34 wrdmap ⊢ P ∈ V ∧ 3 ∈ ℕ 0 → ⟨“ ABC ”⟩ ∈ Word P ∧ ⟨“ ABC ”⟩ = 3 ↔ ⟨“ ABC ”⟩ ∈ P 0 ..^ 3
35 32 33 34 mp2an ⊢ ⟨“ ABC ”⟩ ∈ Word P ∧ ⟨“ ABC ”⟩ = 3 ↔ ⟨“ ABC ”⟩ ∈ P 0 ..^ 3
36 30 31 35 sylanblc ⊢ φ → ⟨“ ABC ”⟩ ∈ P 0 ..^ 3
37 36 biantrurd ⊢ φ → ⟨“ ABC ”⟩ ∼ 𝒢 ⁡ G ⟨“ ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ⟨“ ABC ”⟩ ⁡ 0 ”⟩ ↔ ⟨“ ABC ”⟩ ∈ P 0 ..^ 3 ∧ ⟨“ ABC ”⟩ ∼ 𝒢 ⁡ G ⟨“ ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ⟨“ ABC ”⟩ ⁡ 0 ”⟩
38 s3fv1 ⊢ B ∈ P → ⟨“ ABC ”⟩ ⁡ 1 = B
39 7 38 syl ⊢ φ → ⟨“ ABC ”⟩ ⁡ 1 = B
40 s3fv2 ⊢ C ∈ P → ⟨“ ABC ”⟩ ⁡ 2 = C
41 8 40 syl ⊢ φ → ⟨“ ABC ”⟩ ⁡ 2 = C
42 s3fv0 ⊢ A ∈ P → ⟨“ ABC ”⟩ ⁡ 0 = A
43 6 42 syl ⊢ φ → ⟨“ ABC ”⟩ ⁡ 0 = A
44 39 41 43 s3eqd ⊢ φ → ⟨“ ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ⟨“ ABC ”⟩ ⁡ 0 ”⟩ = ⟨“ BCA ”⟩
45 44 breq2d ⊢ φ → ⟨“ ABC ”⟩ ∼ 𝒢 ⁡ G ⟨“ ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ⟨“ ABC ”⟩ ⁡ 0 ”⟩ ↔ ⟨“ ABC ”⟩ ∼ 𝒢 ⁡ G ⟨“ BCA ”⟩
46 37 45 bitr3d ⊢ φ → ⟨“ ABC ”⟩ ∈ P 0 ..^ 3 ∧ ⟨“ ABC ”⟩ ∼ 𝒢 ⁡ G ⟨“ ⟨“ ABC ”⟩ ⁡ 1 ⟨“ ABC ”⟩ ⁡ 2 ⟨“ ABC ”⟩ ⁡ 0 ”⟩ ↔ ⟨“ ABC ”⟩ ∼ 𝒢 ⁡ G ⟨“ BCA ”⟩
47 21 29 46 3bitrd ⊢ φ → ⟨“ ABC ”⟩ ∈ Equilaterals 𝒢 ⁡ G ↔ ⟨“ ABC ”⟩ ∼ 𝒢 ⁡ G ⟨“ BCA ”⟩