This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tcphcph

Description: The standard definition of a norm turns any pre-Hilbert space over a subfield of CCfld closed under square roots of nonnegative reals into a subcomplex pre-Hilbert space (which allows access to a norm, metric, and topology). (Contributed by Mario Carneiro, 11-Oct-2015)

Ref Expression
Hypotheses tcphval.n 
|- G = ( toCPreHil ` W )
tcphcph.v 
|- V = ( Base ` W )
tcphcph.f 
|- F = ( Scalar ` W )
tcphcph.1 
|- ( ph -> W e. PreHil )
tcphcph.2 
|- ( ph -> F = ( CCfld |`s K ) )
tcphcph.h 
|- ., = ( .i ` W )
tcphcph.3 
|- ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. K )
tcphcph.4 
|- ( ( ph /\ x e. V ) -> 0 <_ ( x ., x ) )
Assertion tcphcph 
|- ( ph -> G e. CPreHil )

Proof

Step Hyp Ref Expression
1 tcphval.n 
 |-  G = ( toCPreHil ` W )
2 tcphcph.v 
 |-  V = ( Base ` W )
3 tcphcph.f 
 |-  F = ( Scalar ` W )
4 tcphcph.1 
 |-  ( ph -> W e. PreHil )
5 tcphcph.2 
 |-  ( ph -> F = ( CCfld |`s K ) )
6 tcphcph.h 
 |-  ., = ( .i ` W )
7 tcphcph.3 
 |-  ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. K )
8 tcphcph.4 
 |-  ( ( ph /\ x e. V ) -> 0 <_ ( x ., x ) )
9 1 tcphphl 
 |-  ( W e. PreHil <-> G e. PreHil )
10 4 9 sylib 
 |-  ( ph -> G e. PreHil )
11 1 2 6 tcphval 
 |-  G = ( W toNrmGrp ( x e. V |-> ( sqrt ` ( x ., x ) ) ) )
12 eqid 
 |-  ( -g ` W ) = ( -g ` W )
13 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
14 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
15 4 14 syl 
 |-  ( ph -> W e. LMod )
16 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
17 15 16 syl 
 |-  ( ph -> W e. Grp )
18 1 2 3 4 5 6 tcphcphlem3 
 |-  ( ( ph /\ x e. V ) -> ( x ., x ) e. RR )
19 18 8 resqrtcld 
 |-  ( ( ph /\ x e. V ) -> ( sqrt ` ( x ., x ) ) e. RR )
20 19 fmpttd 
 |-  ( ph -> ( x e. V |-> ( sqrt ` ( x ., x ) ) ) : V --> RR )
21 oveq12 
 |-  ( ( x = y /\ x = y ) -> ( x ., x ) = ( y ., y ) )
22 21 anidms 
 |-  ( x = y -> ( x ., x ) = ( y ., y ) )
23 22 fveq2d 
 |-  ( x = y -> ( sqrt ` ( x ., x ) ) = ( sqrt ` ( y ., y ) ) )
24 eqid 
 |-  ( x e. V |-> ( sqrt ` ( x ., x ) ) ) = ( x e. V |-> ( sqrt ` ( x ., x ) ) )
25 fvex 
 |-  ( sqrt ` ( x ., x ) ) e. _V
26 23 24 25 fvmpt3i 
 |-  ( y e. V -> ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` y ) = ( sqrt ` ( y ., y ) ) )
27 26 adantl 
 |-  ( ( ph /\ y e. V ) -> ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` y ) = ( sqrt ` ( y ., y ) ) )
28 27 eqeq1d 
 |-  ( ( ph /\ y e. V ) -> ( ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` y ) = 0 <-> ( sqrt ` ( y ., y ) ) = 0 ) )
29 eqid 
 |-  ( Base ` F ) = ( Base ` F )
30 phllvec 
 |-  ( W e. PreHil -> W e. LVec )
31 4 30 syl 
 |-  ( ph -> W e. LVec )
32 3 lvecdrng 
 |-  ( W e. LVec -> F e. DivRing )
33 31 32 syl 
 |-  ( ph -> F e. DivRing )
34 29 5 33 cphsubrglem 
 |-  ( ph -> ( F = ( CCfld |`s ( Base ` F ) ) /\ ( Base ` F ) = ( K i^i CC ) /\ ( Base ` F ) e. ( SubRing ` CCfld ) ) )
35 34 simp2d 
 |-  ( ph -> ( Base ` F ) = ( K i^i CC ) )
36 inss2 
 |-  ( K i^i CC ) C_ CC
37 35 36 eqsstrdi 
 |-  ( ph -> ( Base ` F ) C_ CC )
38 37 adantr 
 |-  ( ( ph /\ y e. V ) -> ( Base ` F ) C_ CC )
39 3 6 2 29 ipcl 
 |-  ( ( W e. PreHil /\ y e. V /\ y e. V ) -> ( y ., y ) e. ( Base ` F ) )
40 39 3anidm23 
 |-  ( ( W e. PreHil /\ y e. V ) -> ( y ., y ) e. ( Base ` F ) )
41 4 40 sylan 
 |-  ( ( ph /\ y e. V ) -> ( y ., y ) e. ( Base ` F ) )
42 38 41 sseldd 
 |-  ( ( ph /\ y e. V ) -> ( y ., y ) e. CC )
43 42 sqrtcld 
 |-  ( ( ph /\ y e. V ) -> ( sqrt ` ( y ., y ) ) e. CC )
44 sqeq0 
 |-  ( ( sqrt ` ( y ., y ) ) e. CC -> ( ( ( sqrt ` ( y ., y ) ) ^ 2 ) = 0 <-> ( sqrt ` ( y ., y ) ) = 0 ) )
45 43 44 syl 
 |-  ( ( ph /\ y e. V ) -> ( ( ( sqrt ` ( y ., y ) ) ^ 2 ) = 0 <-> ( sqrt ` ( y ., y ) ) = 0 ) )
46 42 sqsqrtd 
 |-  ( ( ph /\ y e. V ) -> ( ( sqrt ` ( y ., y ) ) ^ 2 ) = ( y ., y ) )
47 1 2 3 4 5 phclm 
 |-  ( ph -> W e. CMod )
48 3 clm0 
 |-  ( W e. CMod -> 0 = ( 0g ` F ) )
49 47 48 syl 
 |-  ( ph -> 0 = ( 0g ` F ) )
50 49 adantr 
 |-  ( ( ph /\ y e. V ) -> 0 = ( 0g ` F ) )
51 46 50 eqeq12d 
 |-  ( ( ph /\ y e. V ) -> ( ( ( sqrt ` ( y ., y ) ) ^ 2 ) = 0 <-> ( y ., y ) = ( 0g ` F ) ) )
52 45 51 bitr3d 
 |-  ( ( ph /\ y e. V ) -> ( ( sqrt ` ( y ., y ) ) = 0 <-> ( y ., y ) = ( 0g ` F ) ) )
53 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
54 3 6 2 53 13 ipeq0 
 |-  ( ( W e. PreHil /\ y e. V ) -> ( ( y ., y ) = ( 0g ` F ) <-> y = ( 0g ` W ) ) )
55 4 54 sylan 
 |-  ( ( ph /\ y e. V ) -> ( ( y ., y ) = ( 0g ` F ) <-> y = ( 0g ` W ) ) )
56 28 52 55 3bitrd 
 |-  ( ( ph /\ y e. V ) -> ( ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` y ) = 0 <-> y = ( 0g ` W ) ) )
57 4 adantr 
 |-  ( ( ph /\ ( y e. V /\ z e. V ) ) -> W e. PreHil )
58 34 simp1d 
 |-  ( ph -> F = ( CCfld |`s ( Base ` F ) ) )
59 58 adantr 
 |-  ( ( ph /\ ( y e. V /\ z e. V ) ) -> F = ( CCfld |`s ( Base ` F ) ) )
60 3anass 
 |-  ( ( x e. ( Base ` F ) /\ x e. RR /\ 0 <_ x ) <-> ( x e. ( Base ` F ) /\ ( x e. RR /\ 0 <_ x ) ) )
61 simpr2 
 |-  ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> x e. RR )
62 61 recnd 
 |-  ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> x e. CC )
63 62 sqrtcld 
 |-  ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. CC )
64 7 63 jca 
 |-  ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( ( sqrt ` x ) e. K /\ ( sqrt ` x ) e. CC ) )
65 64 ex 
 |-  ( ph -> ( ( x e. K /\ x e. RR /\ 0 <_ x ) -> ( ( sqrt ` x ) e. K /\ ( sqrt ` x ) e. CC ) ) )
66 35 eleq2d 
 |-  ( ph -> ( x e. ( Base ` F ) <-> x e. ( K i^i CC ) ) )
67 recn 
 |-  ( x e. RR -> x e. CC )
68 elin 
 |-  ( x e. ( K i^i CC ) <-> ( x e. K /\ x e. CC ) )
69 68 rbaib 
 |-  ( x e. CC -> ( x e. ( K i^i CC ) <-> x e. K ) )
70 67 69 syl 
 |-  ( x e. RR -> ( x e. ( K i^i CC ) <-> x e. K ) )
71 66 70 sylan9bb 
 |-  ( ( ph /\ x e. RR ) -> ( x e. ( Base ` F ) <-> x e. K ) )
72 71 adantrr 
 |-  ( ( ph /\ ( x e. RR /\ 0 <_ x ) ) -> ( x e. ( Base ` F ) <-> x e. K ) )
73 72 ex 
 |-  ( ph -> ( ( x e. RR /\ 0 <_ x ) -> ( x e. ( Base ` F ) <-> x e. K ) ) )
74 73 pm5.32rd 
 |-  ( ph -> ( ( x e. ( Base ` F ) /\ ( x e. RR /\ 0 <_ x ) ) <-> ( x e. K /\ ( x e. RR /\ 0 <_ x ) ) ) )
75 3anass 
 |-  ( ( x e. K /\ x e. RR /\ 0 <_ x ) <-> ( x e. K /\ ( x e. RR /\ 0 <_ x ) ) )
76 74 75 bitr4di 
 |-  ( ph -> ( ( x e. ( Base ` F ) /\ ( x e. RR /\ 0 <_ x ) ) <-> ( x e. K /\ x e. RR /\ 0 <_ x ) ) )
77 35 eleq2d 
 |-  ( ph -> ( ( sqrt ` x ) e. ( Base ` F ) <-> ( sqrt ` x ) e. ( K i^i CC ) ) )
78 elin 
 |-  ( ( sqrt ` x ) e. ( K i^i CC ) <-> ( ( sqrt ` x ) e. K /\ ( sqrt ` x ) e. CC ) )
79 77 78 bitrdi 
 |-  ( ph -> ( ( sqrt ` x ) e. ( Base ` F ) <-> ( ( sqrt ` x ) e. K /\ ( sqrt ` x ) e. CC ) ) )
80 65 76 79 3imtr4d 
 |-  ( ph -> ( ( x e. ( Base ` F ) /\ ( x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. ( Base ` F ) ) )
81 60 80 biimtrid 
 |-  ( ph -> ( ( x e. ( Base ` F ) /\ x e. RR /\ 0 <_ x ) -> ( sqrt ` x ) e. ( Base ` F ) ) )
82 81 imp 
 |-  ( ( ph /\ ( x e. ( Base ` F ) /\ x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. ( Base ` F ) )
83 82 adantlr 
 |-  ( ( ( ph /\ ( y e. V /\ z e. V ) ) /\ ( x e. ( Base ` F ) /\ x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. ( Base ` F ) )
84 8 adantlr 
 |-  ( ( ( ph /\ ( y e. V /\ z e. V ) ) /\ x e. V ) -> 0 <_ ( x ., x ) )
85 simprl 
 |-  ( ( ph /\ ( y e. V /\ z e. V ) ) -> y e. V )
86 simprr 
 |-  ( ( ph /\ ( y e. V /\ z e. V ) ) -> z e. V )
87 1 2 3 57 59 6 83 84 29 12 85 86 tcphcphlem1 
 |-  ( ( ph /\ ( y e. V /\ z e. V ) ) -> ( sqrt ` ( ( y ( -g ` W ) z ) ., ( y ( -g ` W ) z ) ) ) <_ ( ( sqrt ` ( y ., y ) ) + ( sqrt ` ( z ., z ) ) ) )
88 2 12 grpsubcl 
 |-  ( ( W e. Grp /\ y e. V /\ z e. V ) -> ( y ( -g ` W ) z ) e. V )
89 88 3expb 
 |-  ( ( W e. Grp /\ ( y e. V /\ z e. V ) ) -> ( y ( -g ` W ) z ) e. V )
90 17 89 sylan 
 |-  ( ( ph /\ ( y e. V /\ z e. V ) ) -> ( y ( -g ` W ) z ) e. V )
91 oveq12 
 |-  ( ( x = ( y ( -g ` W ) z ) /\ x = ( y ( -g ` W ) z ) ) -> ( x ., x ) = ( ( y ( -g ` W ) z ) ., ( y ( -g ` W ) z ) ) )
92 91 anidms 
 |-  ( x = ( y ( -g ` W ) z ) -> ( x ., x ) = ( ( y ( -g ` W ) z ) ., ( y ( -g ` W ) z ) ) )
93 92 fveq2d 
 |-  ( x = ( y ( -g ` W ) z ) -> ( sqrt ` ( x ., x ) ) = ( sqrt ` ( ( y ( -g ` W ) z ) ., ( y ( -g ` W ) z ) ) ) )
94 93 24 25 fvmpt3i 
 |-  ( ( y ( -g ` W ) z ) e. V -> ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` ( y ( -g ` W ) z ) ) = ( sqrt ` ( ( y ( -g ` W ) z ) ., ( y ( -g ` W ) z ) ) ) )
95 90 94 syl 
 |-  ( ( ph /\ ( y e. V /\ z e. V ) ) -> ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` ( y ( -g ` W ) z ) ) = ( sqrt ` ( ( y ( -g ` W ) z ) ., ( y ( -g ` W ) z ) ) ) )
96 oveq12 
 |-  ( ( x = z /\ x = z ) -> ( x ., x ) = ( z ., z ) )
97 96 anidms 
 |-  ( x = z -> ( x ., x ) = ( z ., z ) )
98 97 fveq2d 
 |-  ( x = z -> ( sqrt ` ( x ., x ) ) = ( sqrt ` ( z ., z ) ) )
99 98 24 25 fvmpt3i 
 |-  ( z e. V -> ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` z ) = ( sqrt ` ( z ., z ) ) )
100 26 99 oveqan12d 
 |-  ( ( y e. V /\ z e. V ) -> ( ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` y ) + ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` z ) ) = ( ( sqrt ` ( y ., y ) ) + ( sqrt ` ( z ., z ) ) ) )
101 100 adantl 
 |-  ( ( ph /\ ( y e. V /\ z e. V ) ) -> ( ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` y ) + ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` z ) ) = ( ( sqrt ` ( y ., y ) ) + ( sqrt ` ( z ., z ) ) ) )
102 87 95 101 3brtr4d 
 |-  ( ( ph /\ ( y e. V /\ z e. V ) ) -> ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` ( y ( -g ` W ) z ) ) <_ ( ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` y ) + ( ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ` z ) ) )
103 11 2 12 13 17 20 56 102 tngngpd 
 |-  ( ph -> G e. NrmGrp )
104 phllmod 
 |-  ( G e. PreHil -> G e. LMod )
105 10 104 syl 
 |-  ( ph -> G e. LMod )
106 cnnrg 
 |-  CCfld e. NrmRing
107 34 simp3d 
 |-  ( ph -> ( Base ` F ) e. ( SubRing ` CCfld ) )
108 eqid 
 |-  ( CCfld |`s ( Base ` F ) ) = ( CCfld |`s ( Base ` F ) )
109 108 subrgnrg 
 |-  ( ( CCfld e. NrmRing /\ ( Base ` F ) e. ( SubRing ` CCfld ) ) -> ( CCfld |`s ( Base ` F ) ) e. NrmRing )
110 106 107 109 sylancr 
 |-  ( ph -> ( CCfld |`s ( Base ` F ) ) e. NrmRing )
111 58 110 eqeltrd 
 |-  ( ph -> F e. NrmRing )
112 103 105 111 3jca 
 |-  ( ph -> ( G e. NrmGrp /\ G e. LMod /\ F e. NrmRing ) )
113 4 adantr 
 |-  ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) -> W e. PreHil )
114 58 adantr 
 |-  ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) -> F = ( CCfld |`s ( Base ` F ) ) )
115 82 adantlr 
 |-  ( ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) /\ ( x e. ( Base ` F ) /\ x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. ( Base ` F ) )
116 8 adantlr 
 |-  ( ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) /\ x e. V ) -> 0 <_ ( x ., x ) )
117 eqid 
 |-  ( .s ` W ) = ( .s ` W )
118 simprl 
 |-  ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) -> y e. ( Base ` F ) )
119 simprr 
 |-  ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) -> z e. V )
120 1 2 3 113 114 6 115 116 29 117 118 119 tcphcphlem2 
 |-  ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) -> ( sqrt ` ( ( y ( .s ` W ) z ) ., ( y ( .s ` W ) z ) ) ) = ( ( abs ` y ) x. ( sqrt ` ( z ., z ) ) ) )
121 2 3 117 29 lmodvscl 
 |-  ( ( W e. LMod /\ y e. ( Base ` F ) /\ z e. V ) -> ( y ( .s ` W ) z ) e. V )
122 121 3expb 
 |-  ( ( W e. LMod /\ ( y e. ( Base ` F ) /\ z e. V ) ) -> ( y ( .s ` W ) z ) e. V )
123 15 122 sylan 
 |-  ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) -> ( y ( .s ` W ) z ) e. V )
124 eqid 
 |-  ( norm ` G ) = ( norm ` G )
125 1 124 2 6 tcphnmval 
 |-  ( ( W e. Grp /\ ( y ( .s ` W ) z ) e. V ) -> ( ( norm ` G ) ` ( y ( .s ` W ) z ) ) = ( sqrt ` ( ( y ( .s ` W ) z ) ., ( y ( .s ` W ) z ) ) ) )
126 17 123 125 syl2an2r 
 |-  ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) -> ( ( norm ` G ) ` ( y ( .s ` W ) z ) ) = ( sqrt ` ( ( y ( .s ` W ) z ) ., ( y ( .s ` W ) z ) ) ) )
127 114 fveq2d 
 |-  ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) -> ( norm ` F ) = ( norm ` ( CCfld |`s ( Base ` F ) ) ) )
128 127 fveq1d 
 |-  ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) -> ( ( norm ` F ) ` y ) = ( ( norm ` ( CCfld |`s ( Base ` F ) ) ) ` y ) )
129 subrgsubg 
 |-  ( ( Base ` F ) e. ( SubRing ` CCfld ) -> ( Base ` F ) e. ( SubGrp ` CCfld ) )
130 107 129 syl 
 |-  ( ph -> ( Base ` F ) e. ( SubGrp ` CCfld ) )
131 cnfldnm 
 |-  abs = ( norm ` CCfld )
132 eqid 
 |-  ( norm ` ( CCfld |`s ( Base ` F ) ) ) = ( norm ` ( CCfld |`s ( Base ` F ) ) )
133 108 131 132 subgnm2 
 |-  ( ( ( Base ` F ) e. ( SubGrp ` CCfld ) /\ y e. ( Base ` F ) ) -> ( ( norm ` ( CCfld |`s ( Base ` F ) ) ) ` y ) = ( abs ` y ) )
134 130 118 133 syl2an2r 
 |-  ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) -> ( ( norm ` ( CCfld |`s ( Base ` F ) ) ) ` y ) = ( abs ` y ) )
135 128 134 eqtrd 
 |-  ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) -> ( ( norm ` F ) ` y ) = ( abs ` y ) )
136 1 124 2 6 tcphnmval 
 |-  ( ( W e. Grp /\ z e. V ) -> ( ( norm ` G ) ` z ) = ( sqrt ` ( z ., z ) ) )
137 17 119 136 syl2an2r 
 |-  ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) -> ( ( norm ` G ) ` z ) = ( sqrt ` ( z ., z ) ) )
138 135 137 oveq12d 
 |-  ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) -> ( ( ( norm ` F ) ` y ) x. ( ( norm ` G ) ` z ) ) = ( ( abs ` y ) x. ( sqrt ` ( z ., z ) ) ) )
139 120 126 138 3eqtr4d 
 |-  ( ( ph /\ ( y e. ( Base ` F ) /\ z e. V ) ) -> ( ( norm ` G ) ` ( y ( .s ` W ) z ) ) = ( ( ( norm ` F ) ` y ) x. ( ( norm ` G ) ` z ) ) )
140 139 ralrimivva 
 |-  ( ph -> A. y e. ( Base ` F ) A. z e. V ( ( norm ` G ) ` ( y ( .s ` W ) z ) ) = ( ( ( norm ` F ) ` y ) x. ( ( norm ` G ) ` z ) ) )
141 1 2 tcphbas 
 |-  V = ( Base ` G )
142 1 117 tcphvsca 
 |-  ( .s ` W ) = ( .s ` G )
143 1 3 tcphsca 
 |-  F = ( Scalar ` G )
144 eqid 
 |-  ( norm ` F ) = ( norm ` F )
145 141 124 142 143 29 144 isnlm 
 |-  ( G e. NrmMod <-> ( ( G e. NrmGrp /\ G e. LMod /\ F e. NrmRing ) /\ A. y e. ( Base ` F ) A. z e. V ( ( norm ` G ) ` ( y ( .s ` W ) z ) ) = ( ( ( norm ` F ) ` y ) x. ( ( norm ` G ) ` z ) ) ) )
146 112 140 145 sylanbrc 
 |-  ( ph -> G e. NrmMod )
147 10 146 58 3jca 
 |-  ( ph -> ( G e. PreHil /\ G e. NrmMod /\ F = ( CCfld |`s ( Base ` F ) ) ) )
148 elin 
 |-  ( x e. ( ( Base ` F ) i^i ( 0 [,) +oo ) ) <-> ( x e. ( Base ` F ) /\ x e. ( 0 [,) +oo ) ) )
149 elrege0 
 |-  ( x e. ( 0 [,) +oo ) <-> ( x e. RR /\ 0 <_ x ) )
150 149 anbi2i 
 |-  ( ( x e. ( Base ` F ) /\ x e. ( 0 [,) +oo ) ) <-> ( x e. ( Base ` F ) /\ ( x e. RR /\ 0 <_ x ) ) )
151 148 150 bitri 
 |-  ( x e. ( ( Base ` F ) i^i ( 0 [,) +oo ) ) <-> ( x e. ( Base ` F ) /\ ( x e. RR /\ 0 <_ x ) ) )
152 151 80 biimtrid 
 |-  ( ph -> ( x e. ( ( Base ` F ) i^i ( 0 [,) +oo ) ) -> ( sqrt ` x ) e. ( Base ` F ) ) )
153 152 ralrimiv 
 |-  ( ph -> A. x e. ( ( Base ` F ) i^i ( 0 [,) +oo ) ) ( sqrt ` x ) e. ( Base ` F ) )
154 sqrtf 
 |-  sqrt : CC --> CC
155 ffun 
 |-  ( sqrt : CC --> CC -> Fun sqrt )
156 154 155 ax-mp 
 |-  Fun sqrt
157 inss1 
 |-  ( ( Base ` F ) i^i ( 0 [,) +oo ) ) C_ ( Base ` F )
158 157 37 sstrid 
 |-  ( ph -> ( ( Base ` F ) i^i ( 0 [,) +oo ) ) C_ CC )
159 154 fdmi 
 |-  dom sqrt = CC
160 158 159 sseqtrrdi 
 |-  ( ph -> ( ( Base ` F ) i^i ( 0 [,) +oo ) ) C_ dom sqrt )
161 funimass4 
 |-  ( ( Fun sqrt /\ ( ( Base ` F ) i^i ( 0 [,) +oo ) ) C_ dom sqrt ) -> ( ( sqrt " ( ( Base ` F ) i^i ( 0 [,) +oo ) ) ) C_ ( Base ` F ) <-> A. x e. ( ( Base ` F ) i^i ( 0 [,) +oo ) ) ( sqrt ` x ) e. ( Base ` F ) ) )
162 156 160 161 sylancr 
 |-  ( ph -> ( ( sqrt " ( ( Base ` F ) i^i ( 0 [,) +oo ) ) ) C_ ( Base ` F ) <-> A. x e. ( ( Base ` F ) i^i ( 0 [,) +oo ) ) ( sqrt ` x ) e. ( Base ` F ) ) )
163 153 162 mpbird 
 |-  ( ph -> ( sqrt " ( ( Base ` F ) i^i ( 0 [,) +oo ) ) ) C_ ( Base ` F ) )
164 43 fmpttd 
 |-  ( ph -> ( y e. V |-> ( sqrt ` ( y ., y ) ) ) : V --> CC )
165 1 2 6 tcphval 
 |-  G = ( W toNrmGrp ( y e. V |-> ( sqrt ` ( y ., y ) ) ) )
166 cnex 
 |-  CC e. _V
167 165 2 166 tngnm 
 |-  ( ( W e. Grp /\ ( y e. V |-> ( sqrt ` ( y ., y ) ) ) : V --> CC ) -> ( y e. V |-> ( sqrt ` ( y ., y ) ) ) = ( norm ` G ) )
168 17 164 167 syl2anc 
 |-  ( ph -> ( y e. V |-> ( sqrt ` ( y ., y ) ) ) = ( norm ` G ) )
169 168 eqcomd 
 |-  ( ph -> ( norm ` G ) = ( y e. V |-> ( sqrt ` ( y ., y ) ) ) )
170 1 6 tcphip 
 |-  ., = ( .i ` G )
171 141 170 124 143 29 iscph 
 |-  ( G e. CPreHil <-> ( ( G e. PreHil /\ G e. NrmMod /\ F = ( CCfld |`s ( Base ` F ) ) ) /\ ( sqrt " ( ( Base ` F ) i^i ( 0 [,) +oo ) ) ) C_ ( Base ` F ) /\ ( norm ` G ) = ( y e. V |-> ( sqrt ` ( y ., y ) ) ) ) )
172 147 163 169 171 syl3anbrc 
 |-  ( ph -> G e. CPreHil )