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 = ( LineG ` G )
iseqlg.g 
|- ( ph -> G e. TarskiG )
iseqlg.a 
|- ( ph -> A e. P )
iseqlg.b 
|- ( ph -> B e. P )
iseqlg.c 
|- ( ph -> C e. P )
Assertion iseqlg 
|- ( ph -> ( <" A B C "> e. ( eqltrG ` G ) <-> <" A B C "> ( cgrG ` G ) <" B C A "> ) )

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 = ( LineG ` G )
5 iseqlg.g 
 |-  ( ph -> G e. TarskiG )
6 iseqlg.a 
 |-  ( ph -> A e. P )
7 iseqlg.b 
 |-  ( ph -> B e. P )
8 iseqlg.c 
 |-  ( ph -> C e. P )
9 elex 
 |-  ( G e. TarskiG -> G e. _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 ) ^m ( 0 ..^ 3 ) ) = ( P ^m ( 0 ..^ 3 ) ) )
13 fveq2 
 |-  ( g = G -> ( cgrG ` g ) = ( cgrG ` G ) )
14 13 breqd 
 |-  ( g = G -> ( x ( cgrG ` g ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> <-> x ( cgrG ` G ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> ) )
15 12 14 rabeqbidv 
 |-  ( g = G -> { x e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) | x ( cgrG ` g ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> } = { x e. ( P ^m ( 0 ..^ 3 ) ) | x ( cgrG ` G ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> } )
16 df-eqlg 
 |-  eqltrG = ( g e. _V |-> { x e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) | x ( cgrG ` g ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> } )
17 ovex 
 |-  ( P ^m ( 0 ..^ 3 ) ) e. _V
18 17 rabex 
 |-  { x e. ( P ^m ( 0 ..^ 3 ) ) | x ( cgrG ` G ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> } e. _V
19 15 16 18 fvmpt 
 |-  ( G e. _V -> ( eqltrG ` G ) = { x e. ( P ^m ( 0 ..^ 3 ) ) | x ( cgrG ` G ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> } )
20 5 9 19 3syl 
 |-  ( ph -> ( eqltrG ` G ) = { x e. ( P ^m ( 0 ..^ 3 ) ) | x ( cgrG ` G ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> } )
21 20 eleq2d 
 |-  ( ph -> ( <" A B C "> e. ( eqltrG ` G ) <-> <" A B C "> e. { x e. ( P ^m ( 0 ..^ 3 ) ) | x ( cgrG ` G ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> } ) )
22 id 
 |-  ( x = <" A B C "> -> x = <" A B C "> )
23 fveq1 
 |-  ( x = <" A B C "> -> ( x ` 1 ) = ( <" A B C "> ` 1 ) )
24 fveq1 
 |-  ( x = <" A B C "> -> ( x ` 2 ) = ( <" A B C "> ` 2 ) )
25 fveq1 
 |-  ( x = <" A B C "> -> ( x ` 0 ) = ( <" A B C "> ` 0 ) )
26 23 24 25 s3eqd 
 |-  ( x = <" A B C "> -> <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> = <" ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) ( <" A B C "> ` 0 ) "> )
27 22 26 breq12d 
 |-  ( x = <" A B C "> -> ( x ( cgrG ` G ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> <-> <" A B C "> ( cgrG ` G ) <" ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) ( <" A B C "> ` 0 ) "> ) )
28 27 elrab 
 |-  ( <" A B C "> e. { x e. ( P ^m ( 0 ..^ 3 ) ) | x ( cgrG ` G ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> } <-> ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" A B C "> ( cgrG ` G ) <" ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) ( <" A B C "> ` 0 ) "> ) )
29 28 a1i 
 |-  ( ph -> ( <" A B C "> e. { x e. ( P ^m ( 0 ..^ 3 ) ) | x ( cgrG ` G ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> } <-> ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" A B C "> ( cgrG ` G ) <" ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) ( <" A B C "> ` 0 ) "> ) ) )
30 6 7 8 s3cld 
 |-  ( ph -> <" A B C "> e. Word P )
31 s3len 
 |-  ( # ` <" A B C "> ) = 3
32 1 fvexi 
 |-  P e. _V
33 3nn0 
 |-  3 e. NN0
34 wrdmap 
 |-  ( ( P e. _V /\ 3 e. NN0 ) -> ( ( <" A B C "> e. Word P /\ ( # ` <" A B C "> ) = 3 ) <-> <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) ) )
35 32 33 34 mp2an 
 |-  ( ( <" A B C "> e. Word P /\ ( # ` <" A B C "> ) = 3 ) <-> <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) )
36 30 31 35 sylanblc 
 |-  ( ph -> <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) )
37 36 biantrurd 
 |-  ( ph -> ( <" A B C "> ( cgrG ` G ) <" ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) ( <" A B C "> ` 0 ) "> <-> ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" A B C "> ( cgrG ` G ) <" ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) ( <" A B C "> ` 0 ) "> ) ) )
38 s3fv1 
 |-  ( B e. P -> ( <" A B C "> ` 1 ) = B )
39 7 38 syl 
 |-  ( ph -> ( <" A B C "> ` 1 ) = B )
40 s3fv2 
 |-  ( C e. P -> ( <" A B C "> ` 2 ) = C )
41 8 40 syl 
 |-  ( ph -> ( <" A B C "> ` 2 ) = C )
42 s3fv0 
 |-  ( A e. P -> ( <" A B C "> ` 0 ) = A )
43 6 42 syl 
 |-  ( ph -> ( <" A B C "> ` 0 ) = A )
44 39 41 43 s3eqd 
 |-  ( ph -> <" ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) ( <" A B C "> ` 0 ) "> = <" B C A "> )
45 44 breq2d 
 |-  ( ph -> ( <" A B C "> ( cgrG ` G ) <" ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) ( <" A B C "> ` 0 ) "> <-> <" A B C "> ( cgrG ` G ) <" B C A "> ) )
46 37 45 bitr3d 
 |-  ( ph -> ( ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" A B C "> ( cgrG ` G ) <" ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) ( <" A B C "> ` 0 ) "> ) <-> <" A B C "> ( cgrG ` G ) <" B C A "> ) )
47 21 29 46 3bitrd 
 |-  ( ph -> ( <" A B C "> e. ( eqltrG ` G ) <-> <" A B C "> ( cgrG ` G ) <" B C A "> ) )