Metamath Proof Explorer

Theorem rrxnm

Description: The norm of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019)

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

Proof

Step Hyp Ref Expression
1 rrxval.r 
 |-  H = ( RR^ ` I )
2 rrxbase.b 
 |-  B = ( Base ` H )
3 recrng 
 |-  RRfld e. *Ring
4 srngring 
 |-  ( RRfld e. *Ring -> RRfld e. Ring )
5 3 4 ax-mp 
 |-  RRfld e. Ring
6 eqid 
 |-  ( RRfld freeLMod I ) = ( RRfld freeLMod I )
7 6 frlmlmod 
 |-  ( ( RRfld e. Ring /\ I e. V ) -> ( RRfld freeLMod I ) e. LMod )
8 5 7 mpan 
 |-  ( I e. V -> ( RRfld freeLMod I ) e. LMod )
9 lmodgrp 
 |-  ( ( RRfld freeLMod I ) e. LMod -> ( RRfld freeLMod I ) e. Grp )
10 eqid 
 |-  ( toCPreHil ` ( RRfld freeLMod I ) ) = ( toCPreHil ` ( RRfld freeLMod I ) )
11 eqid 
 |-  ( norm ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) = ( norm ` ( toCPreHil ` ( RRfld freeLMod I ) ) )
12 eqid 
 |-  ( Base ` ( RRfld freeLMod I ) ) = ( Base ` ( RRfld freeLMod I ) )
13 eqid 
 |-  ( .i ` ( RRfld freeLMod I ) ) = ( .i ` ( RRfld freeLMod I ) )
14 10 11 12 13 tchnmfval 
 |-  ( ( RRfld freeLMod I ) e. Grp -> ( norm ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) = ( f e. ( Base ` ( RRfld freeLMod I ) ) |-> ( sqrt ` ( f ( .i ` ( RRfld freeLMod I ) ) f ) ) ) )
15 8 9 14 3syl 
 |-  ( I e. V -> ( norm ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) = ( f e. ( Base ` ( RRfld freeLMod I ) ) |-> ( sqrt ` ( f ( .i ` ( RRfld freeLMod I ) ) f ) ) ) )
16 1 rrxval 
 |-  ( I e. V -> H = ( toCPreHil ` ( RRfld freeLMod I ) ) )
17 16 fveq2d 
 |-  ( I e. V -> ( norm ` H ) = ( norm ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
18 16 fveq2d 
 |-  ( I e. V -> ( Base ` H ) = ( Base ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
19 10 12 tcphbas 
 |-  ( Base ` ( RRfld freeLMod I ) ) = ( Base ` ( toCPreHil ` ( RRfld freeLMod I ) ) )
20 18 2 19 3eqtr4g 
 |-  ( I e. V -> B = ( Base ` ( RRfld freeLMod I ) ) )
21 1 2 rrxbase 
 |-  ( I e. V -> B = { f e. ( RR ^m I ) | f finSupp 0 } )
22 ssrab2 
 |-  { f e. ( RR ^m I ) | f finSupp 0 } C_ ( RR ^m I )
23 21 22 eqsstrdi 
 |-  ( I e. V -> B C_ ( RR ^m I ) )
24 23 sselda 
 |-  ( ( I e. V /\ f e. B ) -> f e. ( RR ^m I ) )
25 16 fveq2d 
 |-  ( I e. V -> ( .i ` H ) = ( .i ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
26 1 2 rrxip 
 |-  ( I e. V -> ( h e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( RRfld gsum ( x e. I |-> ( ( h ` x ) x. ( g ` x ) ) ) ) ) = ( .i ` H ) )
27 10 13 tcphip 
 |-  ( .i ` ( RRfld freeLMod I ) ) = ( .i ` ( toCPreHil ` ( RRfld freeLMod I ) ) )
28 27 a1i 
 |-  ( I e. V -> ( .i ` ( RRfld freeLMod I ) ) = ( .i ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
29 25 26 28 3eqtr4rd 
 |-  ( I e. V -> ( .i ` ( RRfld freeLMod I ) ) = ( h e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( RRfld gsum ( x e. I |-> ( ( h ` x ) x. ( g ` x ) ) ) ) ) )
30 29 adantr 
 |-  ( ( I e. V /\ f e. ( RR ^m I ) ) -> ( .i ` ( RRfld freeLMod I ) ) = ( h e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( RRfld gsum ( x e. I |-> ( ( h ` x ) x. ( g ` x ) ) ) ) ) )
31 simprl 
 |-  ( ( ( I e. V /\ f e. ( RR ^m I ) ) /\ ( h = f /\ g = f ) ) -> h = f )
32 31 fveq1d 
 |-  ( ( ( I e. V /\ f e. ( RR ^m I ) ) /\ ( h = f /\ g = f ) ) -> ( h ` x ) = ( f ` x ) )
33 simprr 
 |-  ( ( ( I e. V /\ f e. ( RR ^m I ) ) /\ ( h = f /\ g = f ) ) -> g = f )
34 33 fveq1d 
 |-  ( ( ( I e. V /\ f e. ( RR ^m I ) ) /\ ( h = f /\ g = f ) ) -> ( g ` x ) = ( f ` x ) )
35 32 34 oveq12d 
 |-  ( ( ( I e. V /\ f e. ( RR ^m I ) ) /\ ( h = f /\ g = f ) ) -> ( ( h ` x ) x. ( g ` x ) ) = ( ( f ` x ) x. ( f ` x ) ) )
36 35 adantr 
 |-  ( ( ( ( I e. V /\ f e. ( RR ^m I ) ) /\ ( h = f /\ g = f ) ) /\ x e. I ) -> ( ( h ` x ) x. ( g ` x ) ) = ( ( f ` x ) x. ( f ` x ) ) )
37 elmapi 
 |-  ( f e. ( RR ^m I ) -> f : I --> RR )
38 37 adantl 
 |-  ( ( I e. V /\ f e. ( RR ^m I ) ) -> f : I --> RR )
39 38 ffvelrnda 
 |-  ( ( ( I e. V /\ f e. ( RR ^m I ) ) /\ x e. I ) -> ( f ` x ) e. RR )
40 39 recnd 
 |-  ( ( ( I e. V /\ f e. ( RR ^m I ) ) /\ x e. I ) -> ( f ` x ) e. CC )
41 40 adantlr 
 |-  ( ( ( ( I e. V /\ f e. ( RR ^m I ) ) /\ ( h = f /\ g = f ) ) /\ x e. I ) -> ( f ` x ) e. CC )
42 41 sqvald 
 |-  ( ( ( ( I e. V /\ f e. ( RR ^m I ) ) /\ ( h = f /\ g = f ) ) /\ x e. I ) -> ( ( f ` x ) ^ 2 ) = ( ( f ` x ) x. ( f ` x ) ) )
43 36 42 eqtr4d 
 |-  ( ( ( ( I e. V /\ f e. ( RR ^m I ) ) /\ ( h = f /\ g = f ) ) /\ x e. I ) -> ( ( h ` x ) x. ( g ` x ) ) = ( ( f ` x ) ^ 2 ) )
44 43 mpteq2dva 
 |-  ( ( ( I e. V /\ f e. ( RR ^m I ) ) /\ ( h = f /\ g = f ) ) -> ( x e. I |-> ( ( h ` x ) x. ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) ^ 2 ) ) )
45 44 oveq2d 
 |-  ( ( ( I e. V /\ f e. ( RR ^m I ) ) /\ ( h = f /\ g = f ) ) -> ( RRfld gsum ( x e. I |-> ( ( h ` x ) x. ( g ` x ) ) ) ) = ( RRfld gsum ( x e. I |-> ( ( f ` x ) ^ 2 ) ) ) )
46 simpr 
 |-  ( ( I e. V /\ f e. ( RR ^m I ) ) -> f e. ( RR ^m I ) )
47 ovexd 
 |-  ( ( I e. V /\ f e. ( RR ^m I ) ) -> ( RRfld gsum ( x e. I |-> ( ( f ` x ) ^ 2 ) ) ) e. _V )
48 30 45 46 46 47 ovmpod 
 |-  ( ( I e. V /\ f e. ( RR ^m I ) ) -> ( f ( .i ` ( RRfld freeLMod I ) ) f ) = ( RRfld gsum ( x e. I |-> ( ( f ` x ) ^ 2 ) ) ) )
49 24 48 syldan 
 |-  ( ( I e. V /\ f e. B ) -> ( f ( .i ` ( RRfld freeLMod I ) ) f ) = ( RRfld gsum ( x e. I |-> ( ( f ` x ) ^ 2 ) ) ) )
50 49 eqcomd 
 |-  ( ( I e. V /\ f e. B ) -> ( RRfld gsum ( x e. I |-> ( ( f ` x ) ^ 2 ) ) ) = ( f ( .i ` ( RRfld freeLMod I ) ) f ) )
51 50 fveq2d 
 |-  ( ( I e. V /\ f e. B ) -> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( f ` x ) ^ 2 ) ) ) ) = ( sqrt ` ( f ( .i ` ( RRfld freeLMod I ) ) f ) ) )
52 20 51 mpteq12dva 
 |-  ( I e. V -> ( f e. B |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( f ` x ) ^ 2 ) ) ) ) ) = ( f e. ( Base ` ( RRfld freeLMod I ) ) |-> ( sqrt ` ( f ( .i ` ( RRfld freeLMod I ) ) f ) ) ) )
53 15 17 52 3eqtr4rd 
 |-  ( I e. V -> ( f e. B |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( f ` x ) ^ 2 ) ) ) ) ) = ( norm ` H ) )