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 104 16 eqtr3di
 |-  ( 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 7 frlmsca
 |-  ( ( RRfld e. Field /\ I e. V ) -> RRfld = ( Scalar ` ( RRfld freeLMod I ) ) )
113 14 112 mpan
 |-  ( I e. V -> RRfld = ( Scalar ` ( RRfld freeLMod I ) ) )
114 df-refld
 |-  RRfld = ( CCfld |`s RR )
115 113 114 eqtr3di
 |-  ( 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 )