MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tchcph Unicode version

Theorem tchcph 19147
Description: The standard definition of a norm turns any pre-Hilbert space over a quadratically closed subfield of  CC into a complex pre-Hilbert space (which allows access to a norm, metric, and topology). (Contributed by Mario Carneiro, 11-Oct-2015.)
Hypotheses
Ref Expression
tchval.n  |-  G  =  (toCHil `  W )
tchcph.v  |-  V  =  ( Base `  W
)
tchcph.f  |-  F  =  (Scalar `  W )
tchcph.1  |-  ( ph  ->  W  e.  PreHil )
tchcph.2  |-  ( ph  ->  F  =  (flds  K ) )
tchcph.h  |-  .,  =  ( .i `  W )
tchcph.3  |-  ( (
ph  /\  ( x  e.  K  /\  x  e.  RR  /\  0  <_  x ) )  -> 
( sqr `  x
)  e.  K )
tchcph.4  |-  ( (
ph  /\  x  e.  V )  ->  0  <_  ( x  .,  x
) )
Assertion
Ref Expression
tchcph  |-  ( ph  ->  G  e.  CPreHil )
Distinct variable groups:    x,  .,    x, F   
x, G    x, V    ph, x    x, W
Allowed substitution hint:    K( x)

Proof of Theorem tchcph
Dummy variables  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tchcph.1 . . . 4  |-  ( ph  ->  W  e.  PreHil )
2 tchval.n . . . . 5  |-  G  =  (toCHil `  W )
32tchphl 19138 . . . 4  |-  ( W  e.  PreHil 
<->  G  e.  PreHil )
41, 3sylib 189 . . 3  |-  ( ph  ->  G  e.  PreHil )
5 tchcph.v . . . . . . 7  |-  V  =  ( Base `  W
)
6 tchcph.h . . . . . . 7  |-  .,  =  ( .i `  W )
72, 5, 6tchval 19130 . . . . . 6  |-  G  =  ( W toNrmGrp  ( x  e.  V  |->  ( sqr `  ( x  .,  x
) ) ) )
8 eqid 2404 . . . . . 6  |-  ( -g `  W )  =  (
-g `  W )
9 eqid 2404 . . . . . 6  |-  ( 0g
`  W )  =  ( 0g `  W
)
10 phllmod 16816 . . . . . . . 8  |-  ( W  e.  PreHil  ->  W  e.  LMod )
111, 10syl 16 . . . . . . 7  |-  ( ph  ->  W  e.  LMod )
12 lmodgrp 15912 . . . . . . 7  |-  ( W  e.  LMod  ->  W  e. 
Grp )
1311, 12syl 16 . . . . . 6  |-  ( ph  ->  W  e.  Grp )
14 tchcph.f . . . . . . . . 9  |-  F  =  (Scalar `  W )
15 tchcph.2 . . . . . . . . 9  |-  ( ph  ->  F  =  (flds  K ) )
162, 5, 14, 1, 15, 6tchcphlem3 19143 . . . . . . . 8  |-  ( (
ph  /\  x  e.  V )  ->  (
x  .,  x )  e.  RR )
17 tchcph.4 . . . . . . . 8  |-  ( (
ph  /\  x  e.  V )  ->  0  <_  ( x  .,  x
) )
1816, 17resqrcld 12175 . . . . . . 7  |-  ( (
ph  /\  x  e.  V )  ->  ( sqr `  ( x  .,  x ) )  e.  RR )
19 eqid 2404 . . . . . . 7  |-  ( x  e.  V  |->  ( sqr `  ( x  .,  x
) ) )  =  ( x  e.  V  |->  ( sqr `  (
x  .,  x )
) )
2018, 19fmptd 5852 . . . . . 6  |-  ( ph  ->  ( x  e.  V  |->  ( sqr `  (
x  .,  x )
) ) : V --> RR )
21 oveq12 6049 . . . . . . . . . . . 12  |-  ( ( x  =  y  /\  x  =  y )  ->  ( x  .,  x
)  =  ( y 
.,  y ) )
2221anidms 627 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
x  .,  x )  =  ( y  .,  y ) )
2322fveq2d 5691 . . . . . . . . . 10  |-  ( x  =  y  ->  ( sqr `  ( x  .,  x ) )  =  ( sqr `  (
y  .,  y )
) )
24 fvex 5701 . . . . . . . . . 10  |-  ( sqr `  ( x  .,  x
) )  e.  _V
2523, 19, 24fvmpt3i 5768 . . . . . . . . 9  |-  ( y  e.  V  ->  (
( x  e.  V  |->  ( sqr `  (
x  .,  x )
) ) `  y
)  =  ( sqr `  ( y  .,  y
) ) )
2625adantl 453 . . . . . . . 8  |-  ( (
ph  /\  y  e.  V )  ->  (
( x  e.  V  |->  ( sqr `  (
x  .,  x )
) ) `  y
)  =  ( sqr `  ( y  .,  y
) ) )
2726eqeq1d 2412 . . . . . . 7  |-  ( (
ph  /\  y  e.  V )  ->  (
( ( x  e.  V  |->  ( sqr `  (
x  .,  x )
) ) `  y
)  =  0  <->  ( sqr `  ( y  .,  y ) )  =  0 ) )
28 eqid 2404 . . . . . . . . . . . . . . 15  |-  ( Base `  F )  =  (
Base `  F )
29 phllvec 16815 . . . . . . . . . . . . . . . . 17  |-  ( W  e.  PreHil  ->  W  e.  LVec )
301, 29syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  W  e.  LVec )
3114lvecdrng 16132 . . . . . . . . . . . . . . . 16  |-  ( W  e.  LVec  ->  F  e.  DivRing )
3230, 31syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  e.  DivRing )
3328, 15, 32cphsubrglem 19093 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F  =  (flds  ( Base `  F ) )  /\  ( Base `  F )  =  ( K  i^i  CC )  /\  ( Base `  F )  e.  (SubRing ` fld ) ) )
3433simp2d 970 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Base `  F
)  =  ( K  i^i  CC ) )
35 inss2 3522 . . . . . . . . . . . . 13  |-  ( K  i^i  CC )  C_  CC
3634, 35syl6eqss 3358 . . . . . . . . . . . 12  |-  ( ph  ->  ( Base `  F
)  C_  CC )
3736adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  V )  ->  ( Base `  F )  C_  CC )
3814, 6, 5, 28ipcl 16819 . . . . . . . . . . . . 13  |-  ( ( W  e.  PreHil  /\  y  e.  V  /\  y  e.  V )  ->  (
y  .,  y )  e.  ( Base `  F
) )
39383anidm23 1243 . . . . . . . . . . . 12  |-  ( ( W  e.  PreHil  /\  y  e.  V )  ->  (
y  .,  y )  e.  ( Base `  F
) )
401, 39sylan 458 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  V )  ->  (
y  .,  y )  e.  ( Base `  F
) )
4137, 40sseldd 3309 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  V )  ->  (
y  .,  y )  e.  CC )
4241sqrcld 12194 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  V )  ->  ( sqr `  ( y  .,  y ) )  e.  CC )
43 sqeq0 11401 . . . . . . . . 9  |-  ( ( sqr `  ( y 
.,  y ) )  e.  CC  ->  (
( ( sqr `  (
y  .,  y )
) ^ 2 )  =  0  <->  ( sqr `  ( y  .,  y
) )  =  0 ) )
4442, 43syl 16 . . . . . . . 8  |-  ( (
ph  /\  y  e.  V )  ->  (
( ( sqr `  (
y  .,  y )
) ^ 2 )  =  0  <->  ( sqr `  ( y  .,  y
) )  =  0 ) )
4541sqsqrd 12196 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  V )  ->  (
( sqr `  (
y  .,  y )
) ^ 2 )  =  ( y  .,  y ) )
462, 5, 14, 1, 15tchclm 19142 . . . . . . . . . . 11  |-  ( ph  ->  W  e. CMod )
4714clm0 19050 . . . . . . . . . . 11  |-  ( W  e. CMod  ->  0  =  ( 0g `  F ) )
4846, 47syl 16 . . . . . . . . . 10  |-  ( ph  ->  0  =  ( 0g
`  F ) )
4948adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  V )  ->  0  =  ( 0g `  F ) )
5045, 49eqeq12d 2418 . . . . . . . 8  |-  ( (
ph  /\  y  e.  V )  ->  (
( ( sqr `  (
y  .,  y )
) ^ 2 )  =  0  <->  ( y  .,  y )  =  ( 0g `  F ) ) )
5144, 50bitr3d 247 . . . . . . 7  |-  ( (
ph  /\  y  e.  V )  ->  (
( sqr `  (
y  .,  y )
)  =  0  <->  (
y  .,  y )  =  ( 0g `  F ) ) )
52 eqid 2404 . . . . . . . . 9  |-  ( 0g
`  F )  =  ( 0g `  F
)
5314, 6, 5, 52, 9ipeq0 16824 . . . . . . . 8  |-  ( ( W  e.  PreHil  /\  y  e.  V )  ->  (
( y  .,  y
)  =  ( 0g
`  F )  <->  y  =  ( 0g `  W ) ) )
541, 53sylan 458 . . . . . . 7  |-  ( (
ph  /\  y  e.  V )  ->  (
( y  .,  y
)  =  ( 0g
`  F )  <->  y  =  ( 0g `  W ) ) )
5527, 51, 543bitrd 271 . . . . . 6  |-  ( (
ph  /\  y  e.  V )  ->  (
( ( x  e.  V  |->  ( sqr `  (
x  .,  x )
) ) `  y
)  =  0  <->  y  =  ( 0g `  W ) ) )
561adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  V  /\  z  e.  V ) )  ->  W  e.  PreHil )
5733simp1d 969 . . . . . . . . 9  |-  ( ph  ->  F  =  (flds  ( Base `  F
) ) )
5857adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  V  /\  z  e.  V ) )  ->  F  =  (flds  ( Base `  F
) ) )
59 3anass 940 . . . . . . . . . . 11  |-  ( ( x  e.  ( Base `  F )  /\  x  e.  RR  /\  0  <_  x )  <->  ( x  e.  ( Base `  F
)  /\  ( x  e.  RR  /\  0  <_  x ) ) )
60 tchcph.3 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  K  /\  x  e.  RR  /\  0  <_  x ) )  -> 
( sqr `  x
)  e.  K )
61 simpr2 964 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  K  /\  x  e.  RR  /\  0  <_  x ) )  ->  x  e.  RR )
6261recnd 9070 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  K  /\  x  e.  RR  /\  0  <_  x ) )  ->  x  e.  CC )
6362sqrcld 12194 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  K  /\  x  e.  RR  /\  0  <_  x ) )  -> 
( sqr `  x
)  e.  CC )
6460, 63jca 519 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  K  /\  x  e.  RR  /\  0  <_  x ) )  -> 
( ( sqr `  x
)  e.  K  /\  ( sqr `  x )  e.  CC ) )
6564ex 424 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( x  e.  K  /\  x  e.  RR  /\  0  <_  x )  ->  (
( sqr `  x
)  e.  K  /\  ( sqr `  x )  e.  CC ) ) )
6634eleq2d 2471 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( x  e.  (
Base `  F )  <->  x  e.  ( K  i^i  CC ) ) )
67 recn 9036 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  x  e.  CC )
68 elin 3490 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( K  i^i  CC )  <->  ( x  e.  K  /\  x  e.  CC ) )
6968rbaib 874 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  CC  ->  (
x  e.  ( K  i^i  CC )  <->  x  e.  K ) )
7067, 69syl 16 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  ->  (
x  e.  ( K  i^i  CC )  <->  x  e.  K ) )
7166, 70sylan9bb 681 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  e.  ( Base `  F
)  <->  x  e.  K
) )
7271adantrr 698 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  RR  /\  0  <_  x ) )  -> 
( x  e.  (
Base `  F )  <->  x  e.  K ) )
7372ex 424 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( x  e.  RR  /\  0  <_  x )  ->  (
x  e.  ( Base `  F )  <->  x  e.  K ) ) )
7473pm5.32rd 622 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( x  e.  ( Base `  F
)  /\  ( x  e.  RR  /\  0  <_  x ) )  <->  ( x  e.  K  /\  (
x  e.  RR  /\  0  <_  x ) ) ) )
75 3anass 940 . . . . . . . . . . . . 13  |-  ( ( x  e.  K  /\  x  e.  RR  /\  0  <_  x )  <->  ( x  e.  K  /\  (
x  e.  RR  /\  0  <_  x ) ) )
7674, 75syl6bbr 255 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( x  e.  ( Base `  F
)  /\  ( x  e.  RR  /\  0  <_  x ) )  <->  ( x  e.  K  /\  x  e.  RR  /\  0  <_  x ) ) )
7734eleq2d 2471 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( sqr `  x
)  e.  ( Base `  F )  <->  ( sqr `  x )  e.  ( K  i^i  CC ) ) )
78 elin 3490 . . . . . . . . . . . . 13  |-  ( ( sqr `  x )  e.  ( K  i^i  CC )  <->  ( ( sqr `  x )  e.  K  /\  ( sqr `  x
)  e.  CC ) )
7977, 78syl6bb 253 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( sqr `  x
)  e.  ( Base `  F )  <->  ( ( sqr `  x )  e.  K  /\  ( sqr `  x )  e.  CC ) ) )
8065, 76, 793imtr4d 260 . . . . . . . . . . 11  |-  ( ph  ->  ( ( x  e.  ( Base `  F
)  /\  ( x  e.  RR  /\  0  <_  x ) )  -> 
( sqr `  x
)  e.  ( Base `  F ) ) )
8159, 80syl5bi 209 . . . . . . . . . 10  |-  ( ph  ->  ( ( x  e.  ( Base `  F
)  /\  x  e.  RR  /\  0  <_  x
)  ->  ( sqr `  x )  e.  (
Base `  F )
) )
8281imp 419 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( Base `  F
)  /\  x  e.  RR  /\  0  <_  x
) )  ->  ( sqr `  x )  e.  ( Base `  F
) )
8382adantlr 696 . . . . . . . 8  |-  ( ( ( ph  /\  (
y  e.  V  /\  z  e.  V )
)  /\  ( x  e.  ( Base `  F
)  /\  x  e.  RR  /\  0  <_  x
) )  ->  ( sqr `  x )  e.  ( Base `  F
) )
8417adantlr 696 . . . . . . . 8  |-  ( ( ( ph  /\  (
y  e.  V  /\  z  e.  V )
)  /\  x  e.  V )  ->  0  <_  ( x  .,  x
) )
85 simprl 733 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  V  /\  z  e.  V ) )  -> 
y  e.  V )
86 simprr 734 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  V  /\  z  e.  V ) )  -> 
z  e.  V )
872, 5, 14, 56, 58, 6, 83, 84, 28, 8, 85, 86tchcphlem1 19145 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  V  /\  z  e.  V ) )  -> 
( sqr `  (
( y ( -g `  W ) z ) 
.,  ( y (
-g `  W )
z ) ) )  <_  ( ( sqr `  ( y  .,  y
) )  +  ( sqr `  ( z 
.,  z ) ) ) )
885, 8grpsubcl 14824 . . . . . . . . . 10  |-  ( ( W  e.  Grp  /\  y  e.  V  /\  z  e.  V )  ->  ( y ( -g `  W ) z )  e.  V )
89883expb 1154 . . . . . . . . 9  |-  ( ( W  e.  Grp  /\  ( y  e.  V  /\  z  e.  V
) )  ->  (
y ( -g `  W
) z )  e.  V )
9013, 89sylan 458 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  V  /\  z  e.  V ) )  -> 
( y ( -g `  W ) z )  e.  V )
91 oveq12 6049 . . . . . . . . . . 11  |-  ( ( x  =  ( y ( -g `  W
) z )  /\  x  =  ( y
( -g `  W ) z ) )  -> 
( x  .,  x
)  =  ( ( y ( -g `  W
) z )  .,  ( y ( -g `  W ) z ) ) )
9291anidms 627 . . . . . . . . . 10  |-  ( x  =  ( y (
-g `  W )
z )  ->  (
x  .,  x )  =  ( ( y ( -g `  W
) z )  .,  ( y ( -g `  W ) z ) ) )
9392fveq2d 5691 . . . . . . . . 9  |-  ( x  =  ( y (
-g `  W )
z )  ->  ( sqr `  ( x  .,  x ) )  =  ( sqr `  (
( y ( -g `  W ) z ) 
.,  ( y (
-g `  W )
z ) ) ) )
9493, 19, 24fvmpt3i 5768 . . . . . . . 8  |-  ( ( y ( -g `  W
) z )  e.  V  ->  ( (
x  e.  V  |->  ( sqr `  ( x 
.,  x ) ) ) `  ( y ( -g `  W
) z ) )  =  ( sqr `  (
( y ( -g `  W ) z ) 
.,  ( y (
-g `  W )
z ) ) ) )
9590, 94syl 16 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  V  /\  z  e.  V ) )  -> 
( ( x  e.  V  |->  ( sqr `  (
x  .,  x )
) ) `  (
y ( -g `  W
) z ) )  =  ( sqr `  (
( y ( -g `  W ) z ) 
.,  ( y (
-g `  W )
z ) ) ) )
96 oveq12 6049 . . . . . . . . . . . 12  |-  ( ( x  =  z  /\  x  =  z )  ->  ( x  .,  x
)  =  ( z 
.,  z ) )
9796anidms 627 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
x  .,  x )  =  ( z  .,  z ) )
9897fveq2d 5691 . . . . . . . . . 10  |-  ( x  =  z  ->  ( sqr `  ( x  .,  x ) )  =  ( sqr `  (
z  .,  z )
) )
9998, 19, 24fvmpt3i 5768 . . . . . . . . 9  |-  ( z  e.  V  ->  (
( x  e.  V  |->  ( sqr `  (
x  .,  x )
) ) `  z
)  =  ( sqr `  ( z  .,  z
) ) )
10025, 99oveqan12d 6059 . . . . . . . 8  |-  ( ( y  e.  V  /\  z  e.  V )  ->  ( ( ( x  e.  V  |->  ( sqr `  ( x  .,  x
) ) ) `  y )  +  ( ( x  e.  V  |->  ( sqr `  (
x  .,  x )
) ) `  z
) )  =  ( ( sqr `  (
y  .,  y )
)  +  ( sqr `  ( z  .,  z
) ) ) )
101100adantl 453 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  V  /\  z  e.  V ) )  -> 
( ( ( x  e.  V  |->  ( sqr `  ( x  .,  x
) ) ) `  y )  +  ( ( x  e.  V  |->  ( sqr `  (
x  .,  x )
) ) `  z
) )  =  ( ( sqr `  (
y  .,  y )
)  +  ( sqr `  ( z  .,  z
) ) ) )
10287, 95, 1013brtr4d 4202 . . . . . 6  |-  ( (
ph  /\  ( y  e.  V  /\  z  e.  V ) )  -> 
( ( x  e.  V  |->  ( sqr `  (
x  .,  x )
) ) `  (
y ( -g `  W
) z ) )  <_  ( ( ( x  e.  V  |->  ( sqr `  ( x 
.,  x ) ) ) `  y )  +  ( ( x  e.  V  |->  ( sqr `  ( x  .,  x
) ) ) `  z ) ) )
1037, 5, 8, 9, 13, 20, 55, 102tngngpd 18647 . . . . 5  |-  ( ph  ->  G  e. NrmGrp )
104 phllmod 16816 . . . . . 6  |-  ( G  e.  PreHil  ->  G  e.  LMod )
1054, 104syl 16 . . . . 5  |-  ( ph  ->  G  e.  LMod )
106 cnnrg 18768 . . . . . . 7  |-fld  e. NrmRing
10733simp3d 971 . . . . . . 7  |-  ( ph  ->  ( Base `  F
)  e.  (SubRing ` fld ) )
108 eqid 2404 . . . . . . . 8  |-  (flds  ( Base `  F
) )  =  (flds  ( Base `  F ) )
109108subrgnrg 18662 . . . . . . 7  |-  ( (fld  e. NrmRing  /\  ( Base `  F
)  e.  (SubRing ` fld ) )  ->  (flds  ( Base `  F ) )  e. NrmRing )
110106, 107, 109sylancr 645 . . . . . 6  |-  ( ph  ->  (flds  (
Base `  F )
)  e. NrmRing )
11157, 110eqeltrd 2478 . . . . 5  |-  ( ph  ->  F  e. NrmRing )
112103, 105, 1113jca 1134 . . . 4  |-  ( ph  ->  ( G  e. NrmGrp  /\  G  e.  LMod  /\  F  e. NrmRing ) )
1131adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  ->  W  e.  PreHil )
11457adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  ->  F  =  (flds  ( Base `  F
) ) )
11582adantlr 696 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( Base `  F )  /\  z  e.  V ) )  /\  ( x  e.  ( Base `  F )  /\  x  e.  RR  /\  0  <_  x ) )  -> 
( sqr `  x
)  e.  ( Base `  F ) )
11617adantlr 696 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( Base `  F )  /\  z  e.  V ) )  /\  x  e.  V )  ->  0  <_  ( x  .,  x ) )
117 eqid 2404 . . . . . . 7  |-  ( .s
`  W )  =  ( .s `  W
)
118 simprl 733 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
y  e.  ( Base `  F ) )
119 simprr 734 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
z  e.  V )
1202, 5, 14, 113, 114, 6, 115, 116, 28, 117, 118, 119tchcphlem2 19146 . . . . . 6  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
( sqr `  (
( y ( .s
`  W ) z )  .,  ( y ( .s `  W
) z ) ) )  =  ( ( abs `  y )  x.  ( sqr `  (
z  .,  z )
) ) )
12113adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  ->  W  e.  Grp )
1225, 14, 117, 28lmodvscl 15922 . . . . . . . . 9  |-  ( ( W  e.  LMod  /\  y  e.  ( Base `  F
)  /\  z  e.  V )  ->  (
y ( .s `  W ) z )  e.  V )
1231223expb 1154 . . . . . . . 8  |-  ( ( W  e.  LMod  /\  (
y  e.  ( Base `  F )  /\  z  e.  V ) )  -> 
( y ( .s
`  W ) z )  e.  V )
12411, 123sylan 458 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
( y ( .s
`  W ) z )  e.  V )
125 eqid 2404 . . . . . . . 8  |-  ( norm `  G )  =  (
norm `  G )
1262, 125, 5, 6tchnmval 19140 . . . . . . 7  |-  ( ( W  e.  Grp  /\  ( y ( .s
`  W ) z )  e.  V )  ->  ( ( norm `  G ) `  (
y ( .s `  W ) z ) )  =  ( sqr `  ( ( y ( .s `  W ) z )  .,  (
y ( .s `  W ) z ) ) ) )
127121, 124, 126syl2anc 643 . . . . . 6  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
( ( norm `  G
) `  ( y
( .s `  W
) z ) )  =  ( sqr `  (
( y ( .s
`  W ) z )  .,  ( y ( .s `  W
) z ) ) ) )
128114fveq2d 5691 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
( norm `  F )  =  ( norm `  (flds  ( Base `  F ) ) ) )
129128fveq1d 5689 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
( ( norm `  F
) `  y )  =  ( ( norm `  (flds  (
Base `  F )
) ) `  y
) )
130 subrgsubg 15829 . . . . . . . . . . 11  |-  ( (
Base `  F )  e.  (SubRing ` fld )  ->  ( Base `  F )  e.  (SubGrp ` fld ) )
131107, 130syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( Base `  F
)  e.  (SubGrp ` fld )
)
132131adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
( Base `  F )  e.  (SubGrp ` fld ) )
133 cnfldnm 18766 . . . . . . . . . 10  |-  abs  =  ( norm ` fld )
134 eqid 2404 . . . . . . . . . 10  |-  ( norm `  (flds  (
Base `  F )
) )  =  (
norm `  (flds  ( Base `  F
) ) )
135108, 133, 134subgnm2 18628 . . . . . . . . 9  |-  ( ( ( Base `  F
)  e.  (SubGrp ` fld )  /\  y  e.  ( Base `  F ) )  ->  ( ( norm `  (flds  (
Base `  F )
) ) `  y
)  =  ( abs `  y ) )
136132, 118, 135syl2anc 643 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
( ( norm `  (flds  ( Base `  F ) ) ) `
 y )  =  ( abs `  y
) )
137129, 136eqtrd 2436 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
( ( norm `  F
) `  y )  =  ( abs `  y
) )
1382, 125, 5, 6tchnmval 19140 . . . . . . . 8  |-  ( ( W  e.  Grp  /\  z  e.  V )  ->  ( ( norm `  G
) `  z )  =  ( sqr `  (
z  .,  z )
) )
139121, 119, 138syl2anc 643 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
( ( norm `  G
) `  z )  =  ( sqr `  (
z  .,  z )
) )
140137, 139oveq12d 6058 . . . . . 6  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
( ( ( norm `  F ) `  y
)  x.  ( (
norm `  G ) `  z ) )  =  ( ( abs `  y
)  x.  ( sqr `  ( z  .,  z
) ) ) )
141120, 127, 1403eqtr4d 2446 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
( ( norm `  G
) `  ( y
( .s `  W
) z ) )  =  ( ( (
norm `  F ) `  y )  x.  (
( norm `  G ) `  z ) ) )
142141ralrimivva 2758 . . . 4  |-  ( ph  ->  A. y  e.  (
Base `  F ) A. z  e.  V  ( ( norm `  G
) `  ( y
( .s `  W
) z ) )  =  ( ( (
norm `  F ) `  y )  x.  (
( norm `  G ) `  z ) ) )
1432, 5tchbas 19131 . . . . 5  |-  V  =  ( Base `  G
)
1442, 117tchvsca 19135 . . . . 5  |-  ( .s
`  W )  =  ( .s `  G
)
1452, 14tchsca 19134 . . . . 5  |-  F  =  (Scalar `  G )
146 eqid 2404 . . . . 5  |-  ( norm `  F )  =  (
norm `  F )
147143, 125, 144, 145, 28, 146isnlm 18664 . . . 4  |-  ( 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 )
) ) )
148112, 142, 147sylanbrc 646 . . 3  |-  ( ph  ->  G  e. NrmMod )
1494, 148, 573jca 1134 . 2  |-  ( ph  ->  ( G  e.  PreHil  /\  G  e. NrmMod  /\  F  =  (flds  (
Base `  F )
) ) )
150 elin 3490 . . . . . 6  |-  ( x  e.  ( ( Base `  F )  i^i  (
0 [,)  +oo ) )  <-> 
( x  e.  (
Base `  F )  /\  x  e.  (
0 [,)  +oo ) ) )
151 elrege0 10963 . . . . . . 7  |-  ( x  e.  ( 0 [,) 
+oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
152151anbi2i 676 . . . . . 6  |-  ( ( x  e.  ( Base `  F )  /\  x  e.  ( 0 [,)  +oo ) )  <->  ( x  e.  ( Base `  F
)  /\  ( x  e.  RR  /\  0  <_  x ) ) )
153150, 152bitri 241 . . . . 5  |-  ( x  e.  ( ( Base `  F )  i^i  (
0 [,)  +oo ) )  <-> 
( x  e.  (
Base `  F )  /\  ( x  e.  RR  /\  0  <_  x )
) )
154153, 80syl5bi 209 . . . 4  |-  ( ph  ->  ( x  e.  ( ( Base `  F
)  i^i  ( 0 [,)  +oo ) )  -> 
( sqr `  x
)  e.  ( Base `  F ) ) )
155154ralrimiv 2748 . . 3  |-  ( ph  ->  A. x  e.  ( ( Base `  F
)  i^i  ( 0 [,)  +oo ) ) ( sqr `  x )  e.  ( Base `  F
) )
156 sqrf 12122 . . . . 5  |-  sqr : CC
--> CC
157 ffun 5552 . . . . 5  |-  ( sqr
: CC --> CC  ->  Fun 
sqr )
158156, 157ax-mp 8 . . . 4  |-  Fun  sqr
159 inss1 3521 . . . . . 6  |-  ( (
Base `  F )  i^i  ( 0 [,)  +oo ) )  C_  ( Base `  F )
160159, 36syl5ss 3319 . . . . 5  |-  ( ph  ->  ( ( Base `  F
)  i^i  ( 0 [,)  +oo ) )  C_  CC )
161156fdmi 5555 . . . . 5  |-  dom  sqr  =  CC
162160, 161syl6sseqr 3355 . . . 4  |-  ( ph  ->  ( ( Base `  F
)  i^i  ( 0 [,)  +oo ) )  C_  dom  sqr )
163 funimass4 5736 . . . 4  |-  ( ( Fun  sqr  /\  (
( Base `  F )  i^i  ( 0 [,)  +oo ) )  C_  dom  sqr )  ->  ( ( sqr " ( ( Base `  F )  i^i  (
0 [,)  +oo ) ) )  C_  ( Base `  F )  <->  A. x  e.  ( ( Base `  F
)  i^i  ( 0 [,)  +oo ) ) ( sqr `  x )  e.  ( Base `  F
) ) )
164158, 162, 163sylancr 645 . . 3  |-  ( ph  ->  ( ( sqr " (
( Base `  F )  i^i  ( 0 [,)  +oo ) ) )  C_  ( Base `  F )  <->  A. x  e.  ( (
Base `  F )  i^i  ( 0 [,)  +oo ) ) ( sqr `  x )  e.  (
Base `  F )
) )
165155, 164mpbird 224 . 2  |-  ( ph  ->  ( sqr " (
( Base `  F )  i^i  ( 0 [,)  +oo ) ) )  C_  ( Base `  F )
)
166 eqid 2404 . . . . 5  |-  ( y  e.  V  |->  ( sqr `  ( y  .,  y
) ) )  =  ( y  e.  V  |->  ( sqr `  (
y  .,  y )
) )
16742, 166fmptd 5852 . . . 4  |-  ( ph  ->  ( y  e.  V  |->  ( sqr `  (
y  .,  y )
) ) : V --> CC )
1682, 5, 6tchval 19130 . . . . 5  |-  G  =  ( W toNrmGrp  ( y  e.  V  |->  ( sqr `  ( y  .,  y
) ) ) )
169 cnex 9027 . . . . 5  |-  CC  e.  _V
170168, 5, 169tngnm 18645 . . . 4  |-  ( ( W  e.  Grp  /\  ( y  e.  V  |->  ( sqr `  (
y  .,  y )
) ) : V --> CC )  ->  ( y  e.  V  |->  ( sqr `  ( y  .,  y
) ) )  =  ( norm `  G
) )
17113, 167, 170syl2anc 643 . . 3  |-  ( ph  ->  ( y  e.  V  |->  ( sqr `  (
y  .,  y )
) )  =  (
norm `  G )
)
172171eqcomd 2409 . 2  |-  ( ph  ->  ( norm `  G
)  =  ( y  e.  V  |->  ( sqr `  ( y  .,  y
) ) ) )
1732, 6tchip 19136 . . 3  |-  .,  =  ( .i `  G )
174143, 173, 125, 145, 28iscph 19086 . 2  |-  ( G  e.  CPreHil 
<->  ( ( G  e. 
PreHil  /\  G  e. NrmMod  /\  F  =  (flds  (
Base `  F )
) )  /\  ( sqr " ( ( Base `  F )  i^i  (
0 [,)  +oo ) ) )  C_  ( Base `  F )  /\  ( norm `  G )  =  ( y  e.  V  |->  ( sqr `  (
y  .,  y )
) ) ) )
175149, 165, 172, 174syl3anbrc 1138 1  |-  ( ph  ->  G  e.  CPreHil )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1721   A.wral 2666    i^i cin 3279    C_ wss 3280   class class class wbr 4172    e. cmpt 4226   dom cdm 4837   "cima 4840   Fun wfun 5407   -->wf 5409   ` cfv 5413  (class class class)co 6040   CCcc 8944   RRcr 8945   0cc0 8946    + caddc 8949    x. cmul 8951    +oocpnf 9073    <_ cle 9077   2c2 10005   [,)cico 10874   ^cexp 11337   sqrcsqr 11993   abscabs 11994   Basecbs 13424   ↾s cress 13425  Scalarcsca 13487   .scvsca 13488   .icip 13489   0gc0g 13678   Grpcgrp 14640   -gcsg 14643  SubGrpcsubg 14893   DivRingcdr 15790  SubRingcsubrg 15819   LModclmod 15905   LVecclvec 16129  ℂfldccnfld 16658   PreHilcphl 16810   normcnm 18577  NrmGrpcngp 18578  NrmRingcnrg 18580  NrmModcnlm 18581  CModcclm 19040   CPreHilccph 19082  toCHilctch 19083
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025  ax-mulf 9026
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-tpos 6438  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-q 10531  df-rp 10569  df-xneg 10666  df-xadd 10667  df-xmul 10668  df-ico 10878  df-fz 11000  df-seq 11279  df-exp 11338  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-starv 13499  df-sca 13500  df-vsca 13501  df-ip 13502  df-tset 13503  df-ple 13504  df-ds 13506  df-unif 13507  df-rest 13605  df-topn 13606  df-topgen 13622  df-0g 13682  df-mnd 14645  df-mhm 14693  df-grp 14767  df-minusg 14768  df-sbg 14769  df-subg 14896  df-ghm 14959  df-cmn 15369  df-abl 15370  df-mgp 15604  df-rng 15618  df-cring 15619  df-ur 15620  df-oppr 15683  df-dvdsr 15701  df-unit 15702  df-invr 15732  df-dvr 15743  df-rnghom 15774  df-drng 15792  df-subrg 15821  df-abv 15860  df-staf 15888  df-srng 15889  df-lmod 15907  df-lmhm 16053  df-lvec 16130  df-sra 16199  df-rgmod 16200  df-psmet 16649  df-xmet 16650  df-met 16651  df-bl 16652  df-mopn 16653  df-cnfld 16659  df-phl 16812  df-top 16918  df-bases 16920  df-topon 16921  df-topsp 16922  df-xms 18303  df-ms 18304  df-nm 18583  df-ngp 18584  df-tng 18585  df-nrg 18586  df-nlm 18587  df-clm 19041  df-cph 19084  df-tch 19085
  Copyright terms: Public domain W3C validator