Metamath Proof Explorer

Theorem rrxcph

Description: Generalized Euclidean real spaces are subcomplex pre-Hilbert spaces. (Contributed by Thierry Arnoux, 23-Jun-2019) (Proof shortened by AV, 22-Jul-2019)

Ref Expression
Hypotheses rrxval.r 
|- H = ( RR^ ` I )
rrxbase.b 
|- B = ( Base ` H )
Assertion rrxcph 
|- ( I e. V -> H e. CPreHil )

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 eqid 
 |-  ( toCPreHil ` ( RRfld freeLMod I ) ) = ( toCPreHil ` ( RRfld freeLMod I ) )
5 eqid 
 |-  ( Base ` ( RRfld freeLMod I ) ) = ( Base ` ( RRfld freeLMod I ) )
6 eqid 
 |-  ( Scalar ` ( RRfld freeLMod I ) ) = ( Scalar ` ( RRfld freeLMod I ) )
7 eqid 
 |-  ( RRfld freeLMod I ) = ( RRfld freeLMod I )
8 rebase 
 |-  RR = ( Base ` RRfld )
9 remulr 
 |-  x. = ( .r ` RRfld )
10 eqid 
 |-  ( .i ` ( RRfld freeLMod I ) ) = ( .i ` ( RRfld freeLMod I ) )
11 eqid 
 |-  ( 0g ` ( RRfld freeLMod I ) ) = ( 0g ` ( RRfld freeLMod I ) )
12 re0g 
 |-  0 = ( 0g ` RRfld )
13 refldcj 
 |-  * = ( *r ` RRfld )
14 refld 
 |-  RRfld e. Field
15 14 a1i 
 |-  ( I e. V -> RRfld e. Field )
16 fconstmpt 
 |-  ( I X. { 0 } ) = ( x e. I |-> 0 )
17 7 8 5 frlmbasf 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> f : I --> RR )
18 17 ffnd 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> f Fn I )
19 18 3adant3 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) -> f Fn I )
20 simpl 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> I e. V )
21 14 a1i 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> RRfld e. Field )
22 simpr 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> f e. ( Base ` ( RRfld freeLMod I ) ) )
23 7 8 9 5 10 frlmipval 
 |-  ( ( ( I e. V /\ RRfld e. Field ) /\ ( f e. ( Base ` ( RRfld freeLMod I ) ) /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) ) -> ( f ( .i ` ( RRfld freeLMod I ) ) f ) = ( RRfld gsum ( f oF x. f ) ) )
24 20 21 22 22 23 syl22anc 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( f ( .i ` ( RRfld freeLMod I ) ) f ) = ( RRfld gsum ( f oF x. f ) ) )
25 inidm 
 |-  ( I i^i I ) = I
26 eqidd 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) /\ x e. I ) -> ( f ` x ) = ( f ` x ) )
27 18 18 20 20 25 26 26 offval 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( f oF x. f ) = ( x e. I |-> ( ( f ` x ) x. ( f ` x ) ) ) )
28 17 ffvelrnda 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) /\ x e. I ) -> ( f ` x ) e. RR )
29 28 28 remulcld 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) /\ x e. I ) -> ( ( f ` x ) x. ( f ` x ) ) e. RR )
30 27 29 fmpt3d 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( f oF x. f ) : I --> RR )
31 ovexd 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( f oF x. f ) e. _V )
32 30 ffund 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> Fun ( f oF x. f ) )
33 7 12 5 frlmbasfsupp 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> f finSupp 0 )
34 0red 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> 0 e. RR )
35 simpr 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) /\ x e. RR ) -> x e. RR )
36 35 recnd 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) /\ x e. RR ) -> x e. CC )
37 36 mul02d 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) /\ x e. RR ) -> ( 0 x. x ) = 0 )
38 20 34 17 17 37 suppofss1d 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( ( f oF x. f ) supp 0 ) C_ ( f supp 0 ) )
39 fsuppsssupp 
 |-  ( ( ( ( f oF x. f ) e. _V /\ Fun ( f oF x. f ) ) /\ ( f finSupp 0 /\ ( ( f oF x. f ) supp 0 ) C_ ( f supp 0 ) ) ) -> ( f oF x. f ) finSupp 0 )
40 31 32 33 38 39 syl22anc 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( f oF x. f ) finSupp 0 )
41 regsumsupp 
 |-  ( ( ( f oF x. f ) : I --> RR /\ ( f oF x. f ) finSupp 0 /\ I e. V ) -> ( RRfld gsum ( f oF x. f ) ) = sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f oF x. f ) ` x ) )
42 30 40 20 41 syl3anc 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( RRfld gsum ( f oF x. f ) ) = sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f oF x. f ) ` x ) )
43 suppssdm 
 |-  ( f supp 0 ) C_ dom f
44 43 17 fssdm 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( f supp 0 ) C_ I )
45 38 44 sstrd 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( ( f oF x. f ) supp 0 ) C_ I )
46 45 sselda 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> x e. I )
47 18 18 20 20 25 26 26 ofval 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) /\ x e. I ) -> ( ( f oF x. f ) ` x ) = ( ( f ` x ) x. ( f ` x ) ) )
48 46 47 syldan 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> ( ( f oF x. f ) ` x ) = ( ( f ` x ) x. ( f ` x ) ) )
49 48 sumeq2dv 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f oF x. f ) ` x ) = sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) )
50 42 49 eqtrd 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( RRfld gsum ( f oF x. f ) ) = sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) )
51 24 50 eqtrd 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( f ( .i ` ( RRfld freeLMod I ) ) f ) = sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) )
52 51 3adant3 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) -> ( f ( .i ` ( RRfld freeLMod I ) ) f ) = sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) )
53 simp3 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) -> ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 )
54 52 53 eqtr3d 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) -> sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) = 0 )
55 33 fsuppimpd 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( f supp 0 ) e. Fin )
56 55 38 ssfid 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( ( f oF x. f ) supp 0 ) e. Fin )
57 46 29 syldan 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> ( ( f ` x ) x. ( f ` x ) ) e. RR )
58 28 msqge0d 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) /\ x e. I ) -> 0 <_ ( ( f ` x ) x. ( f ` x ) ) )
59 46 58 syldan 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> 0 <_ ( ( f ` x ) x. ( f ` x ) ) )
60 56 57 59 fsum00 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) = 0 <-> A. x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) = 0 ) )
61 60 3adant3 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) -> ( sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) = 0 <-> A. x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) = 0 ) )
62 54 61 mpbid 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) -> A. x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) = 0 )
63 62 r19.21bi 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> ( ( f ` x ) x. ( f ` x ) ) = 0 )
64 63 adantlr 
 |-  ( ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> ( ( f ` x ) x. ( f ` x ) ) = 0 )
65 28 3adantl3 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( f ` x ) e. RR )
66 65 recnd 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( f ` x ) e. CC )
67 66 66 mul0ord 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( ( ( f ` x ) x. ( f ` x ) ) = 0 <-> ( ( f ` x ) = 0 \/ ( f ` x ) = 0 ) ) )
68 67 adantr 
 |-  ( ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> ( ( ( f ` x ) x. ( f ` x ) ) = 0 <-> ( ( f ` x ) = 0 \/ ( f ` x ) = 0 ) ) )
69 64 68 mpbid 
 |-  ( ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> ( ( f ` x ) = 0 \/ ( f ` x ) = 0 ) )
70 oridm 
 |-  ( ( ( f ` x ) = 0 \/ ( f ` x ) = 0 ) <-> ( f ` x ) = 0 )
71 69 70 sylib 
 |-  ( ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) /\ x e. ( ( f oF x. f ) supp 0 ) ) -> ( f ` x ) = 0 )
72 30 3adant3 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) -> ( f oF x. f ) : I --> RR )
73 72 adantr 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( f oF x. f ) : I --> RR )
74 ssidd 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( ( f oF x. f ) supp 0 ) C_ ( ( f oF x. f ) supp 0 ) )
75 simpl1 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> I e. V )
76 0red 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> 0 e. RR )
77 73 74 75 76 suppssr 
 |-  ( ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) /\ x e. ( I \ ( ( f oF x. f ) supp 0 ) ) ) -> ( ( f oF x. f ) ` x ) = 0 )
78 47 3adantl3 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( ( f oF x. f ) ` x ) = ( ( f ` x ) x. ( f ` x ) ) )
79 78 eqeq1d 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( ( ( f oF x. f ) ` x ) = 0 <-> ( ( f ` x ) x. ( f ` x ) ) = 0 ) )
80 79 67 bitrd 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( ( ( f oF x. f ) ` x ) = 0 <-> ( ( f ` x ) = 0 \/ ( f ` x ) = 0 ) ) )
81 80 70 bitrdi 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( ( ( f oF x. f ) ` x ) = 0 <-> ( f ` x ) = 0 ) )
82 81 biimpa 
 |-  ( ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) /\ ( ( f oF x. f ) ` x ) = 0 ) -> ( f ` x ) = 0 )
83 77 82 syldan 
 |-  ( ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) /\ x e. ( I \ ( ( f oF x. f ) supp 0 ) ) ) -> ( f ` x ) = 0 )
84 undif 
 |-  ( ( ( f oF x. f ) supp 0 ) C_ I <-> ( ( ( f oF x. f ) supp 0 ) u. ( I \ ( ( f oF x. f ) supp 0 ) ) ) = I )
85 45 84 sylib 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( ( ( f oF x. f ) supp 0 ) u. ( I \ ( ( f oF x. f ) supp 0 ) ) ) = I )
86 85 eleq2d 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> ( x e. ( ( ( f oF x. f ) supp 0 ) u. ( I \ ( ( f oF x. f ) supp 0 ) ) ) <-> x e. I ) )
87 86 3adant3 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) -> ( x e. ( ( ( f oF x. f ) supp 0 ) u. ( I \ ( ( f oF x. f ) supp 0 ) ) ) <-> x e. I ) )
88 87 biimpar 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> x e. ( ( ( f oF x. f ) supp 0 ) u. ( I \ ( ( f oF x. f ) supp 0 ) ) ) )
89 elun 
 |-  ( x e. ( ( ( f oF x. f ) supp 0 ) u. ( I \ ( ( f oF x. f ) supp 0 ) ) ) <-> ( x e. ( ( f oF x. f ) supp 0 ) \/ x e. ( I \ ( ( f oF x. f ) supp 0 ) ) ) )
90 88 89 sylib 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( x e. ( ( f oF x. f ) supp 0 ) \/ x e. ( I \ ( ( f oF x. f ) supp 0 ) ) ) )
91 71 83 90 mpjaodan 
 |-  ( ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) /\ x e. I ) -> ( f ` x ) = 0 )
92 91 ralrimiva 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) -> A. x e. I ( f ` x ) = 0 )
93 fconstfv 
 |-  ( f : I --> { 0 } <-> ( f Fn I /\ A. x e. I ( f ` x ) = 0 ) )
94 c0ex 
 |-  0 e. _V
95 94 fconst2 
 |-  ( f : I --> { 0 } <-> f = ( I X. { 0 } ) )
96 93 95 sylbb1 
 |-  ( ( f Fn I /\ A. x e. I ( f ` x ) = 0 ) -> f = ( I X. { 0 } ) )
97 19 92 96 syl2anc 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) -> f = ( I X. { 0 } ) )
98 isfld 
 |-  ( RRfld e. Field <-> ( RRfld e. DivRing /\ RRfld e. CRing ) )
99 14 98 mpbi 
 |-  ( RRfld e. DivRing /\ RRfld e. CRing )
100 99 simpli 
 |-  RRfld e. DivRing
101 drngring 
 |-  ( RRfld e. DivRing -> RRfld e. Ring )
102 100 101 ax-mp 
 |-  RRfld e. Ring
103 7 12 frlm0 
 |-  ( ( RRfld e. Ring /\ I e. V ) -> ( I X. { 0 } ) = ( 0g ` ( RRfld freeLMod I ) ) )
104 102 103 mpan 
 |-  ( I e. V -> ( I X. { 0 } ) = ( 0g ` ( RRfld freeLMod I ) ) )
105 16 104 syl5reqr 
 |-  ( I e. V -> ( 0g ` ( RRfld freeLMod I ) ) = ( x e. I |-> 0 ) )
106 105 3ad2ant1 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) -> ( 0g ` ( RRfld freeLMod I ) ) = ( x e. I |-> 0 ) )
107 16 97 106 3eqtr4a 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) /\ ( f ( .i ` ( RRfld freeLMod I ) ) f ) = 0 ) -> f = ( 0g ` ( RRfld freeLMod I ) ) )
108 cjre 
 |-  ( x e. RR -> ( * ` x ) = x )
109 108 adantl 
 |-  ( ( I e. V /\ x e. RR ) -> ( * ` x ) = x )
110 id 
 |-  ( I e. V -> I e. V )
111 7 8 9 5 10 11 12 13 15 107 109 110 frlmphl 
 |-  ( I e. V -> ( RRfld freeLMod I ) e. PreHil )
112 df-refld 
 |-  RRfld = ( CCfld |`s RR )
113 7 frlmsca 
 |-  ( ( RRfld e. Field /\ I e. V ) -> RRfld = ( Scalar ` ( RRfld freeLMod I ) ) )
114 14 113 mpan 
 |-  ( I e. V -> RRfld = ( Scalar ` ( RRfld freeLMod I ) ) )
115 112 114 syl5reqr 
 |-  ( I e. V -> ( Scalar ` ( RRfld freeLMod I ) ) = ( CCfld |`s RR ) )
116 simpr1 
 |-  ( ( I e. V /\ ( f e. RR /\ f e. RR /\ 0 <_ f ) ) -> f e. RR )
117 simpr3 
 |-  ( ( I e. V /\ ( f e. RR /\ f e. RR /\ 0 <_ f ) ) -> 0 <_ f )
118 116 117 resqrtcld 
 |-  ( ( I e. V /\ ( f e. RR /\ f e. RR /\ 0 <_ f ) ) -> ( sqrt ` f ) e. RR )
119 56 57 59 fsumge0 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> 0 <_ sum_ x e. ( ( f oF x. f ) supp 0 ) ( ( f ` x ) x. ( f ` x ) ) )
120 119 50 breqtrrd 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> 0 <_ ( RRfld gsum ( f oF x. f ) ) )
121 120 24 breqtrrd 
 |-  ( ( I e. V /\ f e. ( Base ` ( RRfld freeLMod I ) ) ) -> 0 <_ ( f ( .i ` ( RRfld freeLMod I ) ) f ) )
122 4 5 6 111 115 10 118 121 tcphcph 
 |-  ( I e. V -> ( toCPreHil ` ( RRfld freeLMod I ) ) e. CPreHil )
123 3 122 eqeltrd 
 |-  ( I e. V -> H e. CPreHil )