# 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}={\mathrm{Base}}_{{G}}$
iseqlg.m
iseqlg.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
iseqlg.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
iseqlg.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
iseqlg.a ${⊢}{\phi }\to {A}\in {P}$
iseqlg.b ${⊢}{\phi }\to {B}\in {P}$
iseqlg.c ${⊢}{\phi }\to {C}\in {P}$
Assertion iseqlg ${⊢}{\phi }\to \left(⟨“{A}{B}{C}”⟩\in {Equilaterals}_{𝒢}\left({G}\right)↔⟨“{A}{B}{C}”⟩{\sim }_{𝒢}\left({G}\right)⟨“{B}{C}{A}”⟩\right)$

### Proof

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