Metamath Proof Explorer

Theorem ecgrtg

Description: The congruence relation used in the Tarski structure for the Euclidean geometry is the same as Cgr . (Contributed by Thierry Arnoux, 15-Mar-2019)

Ref Expression
Hypotheses ecgrtg.1 
|- ( ph -> N e. NN )
ecgrtg.2 
|- P = ( Base ` ( EEG ` N ) )
ecgrtg.3 
|- .- = ( dist ` ( EEG ` N ) )
ecgrtg.a 
|- ( ph -> A e. P )
ecgrtg.b 
|- ( ph -> B e. P )
ecgrtg.c 
|- ( ph -> C e. P )
ecgrtg.d 
|- ( ph -> D e. P )
Assertion ecgrtg 
|- ( ph -> ( <. A , B >. Cgr <. C , D >. <-> ( A .- B ) = ( C .- D ) ) )

Proof

Step Hyp Ref Expression
1 ecgrtg.1 
 |-  ( ph -> N e. NN )
2 ecgrtg.2 
 |-  P = ( Base ` ( EEG ` N ) )
3 ecgrtg.3 
 |-  .- = ( dist ` ( EEG ` N ) )
4 ecgrtg.a 
 |-  ( ph -> A e. P )
5 ecgrtg.b 
 |-  ( ph -> B e. P )
6 ecgrtg.c 
 |-  ( ph -> C e. P )
7 ecgrtg.d 
 |-  ( ph -> D e. P )
8 eengbas 
 |-  ( N e. NN -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) )
9 1 8 syl 
 |-  ( ph -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) )
10 9 2 eqtr4di 
 |-  ( ph -> ( EE ` N ) = P )
11 4 10 eleqtrrd 
 |-  ( ph -> A e. ( EE ` N ) )
12 5 10 eleqtrrd 
 |-  ( ph -> B e. ( EE ` N ) )
13 6 10 eleqtrrd 
 |-  ( ph -> C e. ( EE ` N ) )
14 7 10 eleqtrrd 
 |-  ( ph -> D e. ( EE ` N ) )
15 brcgr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. C , D >. <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
16 11 12 13 14 15 syl22anc 
 |-  ( ph -> ( <. A , B >. Cgr <. C , D >. <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
17 dsid 
 |-  dist = Slot ( dist ` ndx )
18 fvexd 
 |-  ( ph -> ( EEG ` N ) e. _V )
19 eengstr 
 |-  ( N e. NN -> ( EEG ` N ) Struct <. 1 , ; 1 7 >. )
20 1 19 syl 
 |-  ( ph -> ( EEG ` N ) Struct <. 1 , ; 1 7 >. )
21 structn0fun 
 |-  ( ( EEG ` N ) Struct <. 1 , ; 1 7 >. -> Fun ( ( EEG ` N ) \ { (/) } ) )
22 20 21 syl 
 |-  ( ph -> Fun ( ( EEG ` N ) \ { (/) } ) )
23 structcnvcnv 
 |-  ( ( EEG ` N ) Struct <. 1 , ; 1 7 >. -> `' `' ( EEG ` N ) = ( ( EEG ` N ) \ { (/) } ) )
24 20 23 syl 
 |-  ( ph -> `' `' ( EEG ` N ) = ( ( EEG ` N ) \ { (/) } ) )
25 24 funeqd 
 |-  ( ph -> ( Fun `' `' ( EEG ` N ) <-> Fun ( ( EEG ` N ) \ { (/) } ) ) )
26 22 25 mpbird 
 |-  ( ph -> Fun `' `' ( EEG ` N ) )
27 opex 
 |-  <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. e. _V
28 27 prid2 
 |-  <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. e. { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. }
29 elun1 
 |-  ( <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. e. { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } -> <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. e. ( { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } ) )
30 28 29 ax-mp 
 |-  <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. e. ( { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } )
31 eengv 
 |-  ( N e. NN -> ( EEG ` N ) = ( { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } ) )
32 1 31 syl 
 |-  ( ph -> ( EEG ` N ) = ( { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } ) )
33 30 32 eleqtrrid 
 |-  ( ph -> <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. e. ( EEG ` N ) )
34 fvex 
 |-  ( EE ` N ) e. _V
35 34 34 mpoex 
 |-  ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) e. _V
36 35 a1i 
 |-  ( ph -> ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) e. _V )
37 17 18 26 33 36 strfv2d 
 |-  ( ph -> ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) = ( dist ` ( EEG ` N ) ) )
38 3 37 eqtr4id 
 |-  ( ph -> .- = ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) )
39 simplrl 
 |-  ( ( ( ph /\ ( x = A /\ y = B ) ) /\ i e. ( 1 ... N ) ) -> x = A )
40 39 fveq1d 
 |-  ( ( ( ph /\ ( x = A /\ y = B ) ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) = ( A ` i ) )
41 simplrr 
 |-  ( ( ( ph /\ ( x = A /\ y = B ) ) /\ i e. ( 1 ... N ) ) -> y = B )
42 41 fveq1d 
 |-  ( ( ( ph /\ ( x = A /\ y = B ) ) /\ i e. ( 1 ... N ) ) -> ( y ` i ) = ( B ` i ) )
43 40 42 oveq12d 
 |-  ( ( ( ph /\ ( x = A /\ y = B ) ) /\ i e. ( 1 ... N ) ) -> ( ( x ` i ) - ( y ` i ) ) = ( ( A ` i ) - ( B ` i ) ) )
44 43 oveq1d 
 |-  ( ( ( ph /\ ( x = A /\ y = B ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) = ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) )
45 44 sumeq2dv 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) )
46 sumex 
 |-  sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) e. _V
47 46 a1i 
 |-  ( ph -> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) e. _V )
48 38 45 11 12 47 ovmpod 
 |-  ( ph -> ( A .- B ) = sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) )
49 48 eqcomd 
 |-  ( ph -> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = ( A .- B ) )
50 simplrl 
 |-  ( ( ( ph /\ ( x = C /\ y = D ) ) /\ i e. ( 1 ... N ) ) -> x = C )
51 50 fveq1d 
 |-  ( ( ( ph /\ ( x = C /\ y = D ) ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) = ( C ` i ) )
52 simplrr 
 |-  ( ( ( ph /\ ( x = C /\ y = D ) ) /\ i e. ( 1 ... N ) ) -> y = D )
53 52 fveq1d 
 |-  ( ( ( ph /\ ( x = C /\ y = D ) ) /\ i e. ( 1 ... N ) ) -> ( y ` i ) = ( D ` i ) )
54 51 53 oveq12d 
 |-  ( ( ( ph /\ ( x = C /\ y = D ) ) /\ i e. ( 1 ... N ) ) -> ( ( x ` i ) - ( y ` i ) ) = ( ( C ` i ) - ( D ` i ) ) )
55 54 oveq1d 
 |-  ( ( ( ph /\ ( x = C /\ y = D ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) = ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) )
56 55 sumeq2dv 
 |-  ( ( ph /\ ( x = C /\ y = D ) ) -> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) )
57 sumex 
 |-  sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) e. _V
58 57 a1i 
 |-  ( ph -> sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) e. _V )
59 38 56 13 14 58 ovmpod 
 |-  ( ph -> ( C .- D ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) )
60 59 eqcomd 
 |-  ( ph -> sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) = ( C .- D ) )
61 49 60 eqeq12d 
 |-  ( ph -> ( sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) <-> ( A .- B ) = ( C .- D ) ) )
62 16 61 bitrd 
 |-  ( ph -> ( <. A , B >. Cgr <. C , D >. <-> ( A .- B ) = ( C .- D ) ) )