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 syl6eqr 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 ”⟩