Metamath Proof Explorer

Theorem axcgrid

Description: If there is no distance between A and B , then A = B . Axiom A3 of Schwabhauser p. 10. (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion axcgrid 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. C , C >. -> A = B ) )

Proof

Step Hyp Ref Expression
1 fveecn 
 |-  ( ( C e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. CC )
2 subid 
 |-  ( ( C ` i ) e. CC -> ( ( C ` i ) - ( C ` i ) ) = 0 )
3 2 sq0id 
 |-  ( ( C ` i ) e. CC -> ( ( ( C ` i ) - ( C ` i ) ) ^ 2 ) = 0 )
4 1 3 syl 
 |-  ( ( C e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( ( ( C ` i ) - ( C ` i ) ) ^ 2 ) = 0 )
5 4 sumeq2dv 
 |-  ( C e. ( EE ` N ) -> sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( C ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) 0 )
6 fzfid 
 |-  ( C e. ( EE ` N ) -> ( 1 ... N ) e. Fin )
7 sumz 
 |-  ( ( ( 1 ... N ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... N ) e. Fin ) -> sum_ i e. ( 1 ... N ) 0 = 0 )
8 7 olcs 
 |-  ( ( 1 ... N ) e. Fin -> sum_ i e. ( 1 ... N ) 0 = 0 )
9 6 8 syl 
 |-  ( C e. ( EE ` N ) -> sum_ i e. ( 1 ... N ) 0 = 0 )
10 5 9 eqtrd 
 |-  ( C e. ( EE ` N ) -> sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( C ` i ) ) ^ 2 ) = 0 )
11 10 3ad2ant3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( C ` i ) ) ^ 2 ) = 0 )
12 11 eqeq2d 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( C ` i ) ) ^ 2 ) <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 ) )
13 fzfid 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( 1 ... N ) e. Fin )
14 fveere 
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
15 14 adantlr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
16 fveere 
 |-  ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR )
17 16 adantll 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR )
18 15 17 resubcld 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) - ( B ` i ) ) e. RR )
19 18 resqcld 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) e. RR )
20 18 sqge0d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> 0 <_ ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) )
21 13 19 20 fsum00 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 <-> A. i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 ) )
22 fveecn 
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
23 fveecn 
 |-  ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. CC )
24 subcl 
 |-  ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) -> ( ( A ` i ) - ( B ` i ) ) e. CC )
25 sqeq0 
 |-  ( ( ( A ` i ) - ( B ` i ) ) e. CC -> ( ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 <-> ( ( A ` i ) - ( B ` i ) ) = 0 ) )
26 24 25 syl 
 |-  ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) -> ( ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 <-> ( ( A ` i ) - ( B ` i ) ) = 0 ) )
27 subeq0 
 |-  ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) -> ( ( ( A ` i ) - ( B ` i ) ) = 0 <-> ( A ` i ) = ( B ` i ) ) )
28 26 27 bitrd 
 |-  ( ( ( A ` i ) e. CC /\ ( B ` i ) e. CC ) -> ( ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 <-> ( A ` i ) = ( B ` i ) ) )
29 22 23 28 syl2an 
 |-  ( ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) /\ ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) ) -> ( ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 <-> ( A ` i ) = ( B ` i ) ) )
30 29 anandirs 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 <-> ( A ` i ) = ( B ` i ) ) )
31 30 ralbidva 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A. i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
32 21 31 bitrd 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
33 32 3adant3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
34 12 33 bitrd 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( C ` i ) ) ^ 2 ) <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
35 simp1 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> A e. ( EE ` N ) )
36 simp2 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> B e. ( EE ` N ) )
37 simp3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> C e. ( EE ` N ) )
38 brcgr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. C , C >. <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( C ` i ) ) ^ 2 ) ) )
39 35 36 37 37 38 syl22anc 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( <. A , B >. Cgr <. C , C >. <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( C ` i ) ) ^ 2 ) ) )
40 eqeefv 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
41 40 3adant3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
42 34 39 41 3bitr4d 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( <. A , B >. Cgr <. C , C >. <-> A = B ) )
43 42 biimpd 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( <. A , B >. Cgr <. C , C >. -> A = B ) )
44 43 adantl 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. C , C >. -> A = B ) )