Metamath Proof Explorer

Theorem rrxds

Description: The distance over generalized Euclidean spaces. Compare with df-rrn . (Contributed by Thierry Arnoux, 20-Jun-2019) (Proof shortened by AV, 20-Jul-2019)

Ref Expression
Hypotheses rrxval.r 
|- H = ( RR^ ` I )
rrxbase.b 
|- B = ( Base ` H )
Assertion rrxds 
|- ( I e. V -> ( f e. B , g e. B |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) = ( dist ` H ) )

Proof

Step Hyp Ref Expression
1 rrxval.r 
 |-  H = ( RR^ ` I )
2 rrxbase.b 
 |-  B = ( Base ` H )
3 1 rrxval 
 |-  ( I e. V -> H = ( toCPreHil ` ( RRfld freeLMod I ) ) )
4 3 fveq2d 
 |-  ( I e. V -> ( dist ` H ) = ( dist ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
5 recrng 
 |-  RRfld e. *Ring
6 srngring 
 |-  ( RRfld e. *Ring -> RRfld e. Ring )
7 5 6 ax-mp 
 |-  RRfld e. Ring
8 eqid 
 |-  ( RRfld freeLMod I ) = ( RRfld freeLMod I )
9 8 frlmlmod 
 |-  ( ( RRfld e. Ring /\ I e. V ) -> ( RRfld freeLMod I ) e. LMod )
10 7 9 mpan 
 |-  ( I e. V -> ( RRfld freeLMod I ) e. LMod )
11 lmodgrp 
 |-  ( ( RRfld freeLMod I ) e. LMod -> ( RRfld freeLMod I ) e. Grp )
12 eqid 
 |-  ( toCPreHil ` ( RRfld freeLMod I ) ) = ( toCPreHil ` ( RRfld freeLMod I ) )
13 eqid 
 |-  ( norm ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) = ( norm ` ( toCPreHil ` ( RRfld freeLMod I ) ) )
14 eqid 
 |-  ( -g ` ( RRfld freeLMod I ) ) = ( -g ` ( RRfld freeLMod I ) )
15 12 13 14 tcphds 
 |-  ( ( RRfld freeLMod I ) e. Grp -> ( ( norm ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) o. ( -g ` ( RRfld freeLMod I ) ) ) = ( dist ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
16 10 11 15 3syl 
 |-  ( I e. V -> ( ( norm ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) o. ( -g ` ( RRfld freeLMod I ) ) ) = ( dist ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
17 eqid 
 |-  ( Base ` ( RRfld freeLMod I ) ) = ( Base ` ( RRfld freeLMod I ) )
18 17 14 grpsubf 
 |-  ( ( RRfld freeLMod I ) e. Grp -> ( -g ` ( RRfld freeLMod I ) ) : ( ( Base ` ( RRfld freeLMod I ) ) X. ( Base ` ( RRfld freeLMod I ) ) ) --> ( Base ` ( RRfld freeLMod I ) ) )
19 10 11 18 3syl 
 |-  ( I e. V -> ( -g ` ( RRfld freeLMod I ) ) : ( ( Base ` ( RRfld freeLMod I ) ) X. ( Base ` ( RRfld freeLMod I ) ) ) --> ( Base ` ( RRfld freeLMod I ) ) )
20 1 2 rrxbase 
 |-  ( I e. V -> B = { h e. ( RR ^m I ) | h finSupp 0 } )
21 rebase 
 |-  RR = ( Base ` RRfld )
22 re0g 
 |-  0 = ( 0g ` RRfld )
23 eqid 
 |-  { h e. ( RR ^m I ) | h finSupp 0 } = { h e. ( RR ^m I ) | h finSupp 0 }
24 8 21 22 23 frlmbas 
 |-  ( ( RRfld e. Ring /\ I e. V ) -> { h e. ( RR ^m I ) | h finSupp 0 } = ( Base ` ( RRfld freeLMod I ) ) )
25 7 24 mpan 
 |-  ( I e. V -> { h e. ( RR ^m I ) | h finSupp 0 } = ( Base ` ( RRfld freeLMod I ) ) )
26 20 25 eqtrd 
 |-  ( I e. V -> B = ( Base ` ( RRfld freeLMod I ) ) )
27 26 sqxpeqd 
 |-  ( I e. V -> ( B X. B ) = ( ( Base ` ( RRfld freeLMod I ) ) X. ( Base ` ( RRfld freeLMod I ) ) ) )
28 27 26 feq23d 
 |-  ( I e. V -> ( ( -g ` ( RRfld freeLMod I ) ) : ( B X. B ) --> B <-> ( -g ` ( RRfld freeLMod I ) ) : ( ( Base ` ( RRfld freeLMod I ) ) X. ( Base ` ( RRfld freeLMod I ) ) ) --> ( Base ` ( RRfld freeLMod I ) ) ) )
29 19 28 mpbird 
 |-  ( I e. V -> ( -g ` ( RRfld freeLMod I ) ) : ( B X. B ) --> B )
30 29 fovrnda 
 |-  ( ( I e. V /\ ( f e. B /\ g e. B ) ) -> ( f ( -g ` ( RRfld freeLMod I ) ) g ) e. B )
31 29 ffnd 
 |-  ( I e. V -> ( -g ` ( RRfld freeLMod I ) ) Fn ( B X. B ) )
32 fnov 
 |-  ( ( -g ` ( RRfld freeLMod I ) ) Fn ( B X. B ) <-> ( -g ` ( RRfld freeLMod I ) ) = ( f e. B , g e. B |-> ( f ( -g ` ( RRfld freeLMod I ) ) g ) ) )
33 31 32 sylib 
 |-  ( I e. V -> ( -g ` ( RRfld freeLMod I ) ) = ( f e. B , g e. B |-> ( f ( -g ` ( RRfld freeLMod I ) ) g ) ) )
34 1 2 rrxnm 
 |-  ( I e. V -> ( h e. B |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( h ` x ) ^ 2 ) ) ) ) ) = ( norm ` H ) )
35 3 fveq2d 
 |-  ( I e. V -> ( norm ` H ) = ( norm ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
36 34 35 eqtr2d 
 |-  ( I e. V -> ( norm ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) = ( h e. B |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( h ` x ) ^ 2 ) ) ) ) ) )
37 fveq1 
 |-  ( h = ( f ( -g ` ( RRfld freeLMod I ) ) g ) -> ( h ` x ) = ( ( f ( -g ` ( RRfld freeLMod I ) ) g ) ` x ) )
38 37 oveq1d 
 |-  ( h = ( f ( -g ` ( RRfld freeLMod I ) ) g ) -> ( ( h ` x ) ^ 2 ) = ( ( ( f ( -g ` ( RRfld freeLMod I ) ) g ) ` x ) ^ 2 ) )
39 38 mpteq2dv 
 |-  ( h = ( f ( -g ` ( RRfld freeLMod I ) ) g ) -> ( x e. I |-> ( ( h ` x ) ^ 2 ) ) = ( x e. I |-> ( ( ( f ( -g ` ( RRfld freeLMod I ) ) g ) ` x ) ^ 2 ) ) )
40 39 oveq2d 
 |-  ( h = ( f ( -g ` ( RRfld freeLMod I ) ) g ) -> ( RRfld gsum ( x e. I |-> ( ( h ` x ) ^ 2 ) ) ) = ( RRfld gsum ( x e. I |-> ( ( ( f ( -g ` ( RRfld freeLMod I ) ) g ) ` x ) ^ 2 ) ) ) )
41 40 fveq2d 
 |-  ( h = ( f ( -g ` ( RRfld freeLMod I ) ) g ) -> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( h ` x ) ^ 2 ) ) ) ) = ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ( -g ` ( RRfld freeLMod I ) ) g ) ` x ) ^ 2 ) ) ) ) )
42 30 33 36 41 fmpoco 
 |-  ( I e. V -> ( ( norm ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) o. ( -g ` ( RRfld freeLMod I ) ) ) = ( f e. B , g e. B |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ( -g ` ( RRfld freeLMod I ) ) g ) ` x ) ^ 2 ) ) ) ) ) )
43 simp1 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> I e. V )
44 simprl 
 |-  ( ( I e. V /\ ( f e. B /\ g e. B ) ) -> f e. B )
45 26 adantr 
 |-  ( ( I e. V /\ ( f e. B /\ g e. B ) ) -> B = ( Base ` ( RRfld freeLMod I ) ) )
46 44 45 eleqtrd 
 |-  ( ( I e. V /\ ( f e. B /\ g e. B ) ) -> f e. ( Base ` ( RRfld freeLMod I ) ) )
47 46 3impb 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> f e. ( Base ` ( RRfld freeLMod I ) ) )
48 8 21 17 frlmbasmap 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> f e. ( RR ^m I ) )
49 43 47 48 syl2anc 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> f e. ( RR ^m I ) )
50 elmapi 
 |-  ( f e. ( RR ^m I ) -> f : I --> RR )
51 49 50 syl 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> f : I --> RR )
52 51 ffnd 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> f Fn I )
53 simprr 
 |-  ( ( I e. V /\ ( f e. B /\ g e. B ) ) -> g e. B )
54 53 45 eleqtrd 
 |-  ( ( I e. V /\ ( f e. B /\ g e. B ) ) -> g e. ( Base ` ( RRfld freeLMod I ) ) )
55 54 3impb 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> g e. ( Base ` ( RRfld freeLMod I ) ) )
56 8 21 17 frlmbasmap 
 |-  ( ( I e. V /\ g e. ( Base ` ( RRfld freeLMod I ) ) ) -> g e. ( RR ^m I ) )
57 43 55 56 syl2anc 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> g e. ( RR ^m I ) )
58 elmapi 
 |-  ( g e. ( RR ^m I ) -> g : I --> RR )
59 57 58 syl 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> g : I --> RR )
60 59 ffnd 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> g Fn I )
61 inidm 
 |-  ( I i^i I ) = I
62 eqidd 
 |-  ( ( ( I e. V /\ f e. B /\ g e. B ) /\ x e. I ) -> ( f ` x ) = ( f ` x ) )
63 eqidd 
 |-  ( ( ( I e. V /\ f e. B /\ g e. B ) /\ x e. I ) -> ( g ` x ) = ( g ` x ) )
64 52 60 43 43 61 62 63 offval 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> ( f oF ( -g ` RRfld ) g ) = ( x e. I |-> ( ( f ` x ) ( -g ` RRfld ) ( g ` x ) ) ) )
65 7 a1i 
 |-  ( ( I e. V /\ ( f e. B /\ g e. B ) ) -> RRfld e. Ring )
66 simpl 
 |-  ( ( I e. V /\ ( f e. B /\ g e. B ) ) -> I e. V )
67 eqid 
 |-  ( -g ` RRfld ) = ( -g ` RRfld )
68 8 17 65 66 46 54 67 14 frlmsubgval 
 |-  ( ( I e. V /\ ( f e. B /\ g e. B ) ) -> ( f ( -g ` ( RRfld freeLMod I ) ) g ) = ( f oF ( -g ` RRfld ) g ) )
69 68 3impb 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> ( f ( -g ` ( RRfld freeLMod I ) ) g ) = ( f oF ( -g ` RRfld ) g ) )
70 51 ffvelrnda 
 |-  ( ( ( I e. V /\ f e. B /\ g e. B ) /\ x e. I ) -> ( f ` x ) e. RR )
71 59 ffvelrnda 
 |-  ( ( ( I e. V /\ f e. B /\ g e. B ) /\ x e. I ) -> ( g ` x ) e. RR )
72 67 resubgval 
 |-  ( ( ( f ` x ) e. RR /\ ( g ` x ) e. RR ) -> ( ( f ` x ) - ( g ` x ) ) = ( ( f ` x ) ( -g ` RRfld ) ( g ` x ) ) )
73 70 71 72 syl2anc 
 |-  ( ( ( I e. V /\ f e. B /\ g e. B ) /\ x e. I ) -> ( ( f ` x ) - ( g ` x ) ) = ( ( f ` x ) ( -g ` RRfld ) ( g ` x ) ) )
74 73 mpteq2dva 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> ( x e. I |-> ( ( f ` x ) - ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) ( -g ` RRfld ) ( g ` x ) ) ) )
75 64 69 74 3eqtr4d 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> ( f ( -g ` ( RRfld freeLMod I ) ) g ) = ( x e. I |-> ( ( f ` x ) - ( g ` x ) ) ) )
76 70 71 resubcld 
 |-  ( ( ( I e. V /\ f e. B /\ g e. B ) /\ x e. I ) -> ( ( f ` x ) - ( g ` x ) ) e. RR )
77 75 76 fvmpt2d 
 |-  ( ( ( I e. V /\ f e. B /\ g e. B ) /\ x e. I ) -> ( ( f ( -g ` ( RRfld freeLMod I ) ) g ) ` x ) = ( ( f ` x ) - ( g ` x ) ) )
78 77 oveq1d 
 |-  ( ( ( I e. V /\ f e. B /\ g e. B ) /\ x e. I ) -> ( ( ( f ( -g ` ( RRfld freeLMod I ) ) g ) ` x ) ^ 2 ) = ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) )
79 78 mpteq2dva 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> ( x e. I |-> ( ( ( f ( -g ` ( RRfld freeLMod I ) ) g ) ` x ) ^ 2 ) ) = ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) )
80 79 oveq2d 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> ( RRfld gsum ( x e. I |-> ( ( ( f ( -g ` ( RRfld freeLMod I ) ) g ) ` x ) ^ 2 ) ) ) = ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) )
81 80 fveq2d 
 |-  ( ( I e. V /\ f e. B /\ g e. B ) -> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ( -g ` ( RRfld freeLMod I ) ) g ) ` x ) ^ 2 ) ) ) ) = ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) )
82 81 mpoeq3dva 
 |-  ( I e. V -> ( f e. B , g e. B |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ( -g ` ( RRfld freeLMod I ) ) g ) ` x ) ^ 2 ) ) ) ) ) = ( f e. B , g e. B |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) )
83 42 82 eqtrd 
 |-  ( I e. V -> ( ( norm ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) o. ( -g ` ( RRfld freeLMod I ) ) ) = ( f e. B , g e. B |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) )
84 4 16 83 3eqtr2rd 
 |-  ( I e. V -> ( f e. B , g e. B |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) = ( dist ` H ) )