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

Theorem tchcph 19058
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 19049 . . . 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 19041 . . . . . 6  |-  G  =  ( W toNrmGrp  ( x  e.  V  |->  ( sqr `  ( x  .,  x
) ) ) )
8 eqid 2380 . . . . . 6  |-  ( -g `  W )  =  (
-g `  W )
9 eqid 2380 . . . . . 6  |-  ( 0g
`  W )  =  ( 0g `  W
)
10 phllmod 16777 . . . . . . . 8  |-  ( W  e.  PreHil  ->  W  e.  LMod )
111, 10syl 16 . . . . . . 7  |-  ( ph  ->  W  e.  LMod )
12 lmodgrp 15877 . . . . . . 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 19054 . . . . . . . 8  |-  ( (
ph  /\  x  e.  V )  ->  (
x  .,  x )  e.  RR )
17 tchcph.4 . . . . . . . 8  |-  ( (
ph  /\  x  e.  V )  ->  0  <_  ( x  .,  x
) )
1816, 17resqrcld 12140 . . . . . . 7  |-  ( (
ph  /\  x  e.  V )  ->  ( sqr `  ( x  .,  x ) )  e.  RR )
19 eqid 2380 . . . . . . 7  |-  ( x  e.  V  |->  ( sqr `  ( x  .,  x
) ) )  =  ( x  e.  V  |->  ( sqr `  (
x  .,  x )
) )
2018, 19fmptd 5825 . . . . . 6  |-  ( ph  ->  ( x  e.  V  |->  ( sqr `  (
x  .,  x )
) ) : V --> RR )
21 oveq12 6022 . . . . . . . . . . . 12  |-  ( ( x  =  y  /\  x  =  y )  ->  ( x  .,  x
)  =  ( y 
.,  y ) )
2221anidms 627 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
x  .,  x )  =  ( y  .,  y ) )
2322fveq2d 5665 . . . . . . . . . 10  |-  ( x  =  y  ->  ( sqr `  ( x  .,  x ) )  =  ( sqr `  (
y  .,  y )
) )
24 fvex 5675 . . . . . . . . . 10  |-  ( sqr `  ( x  .,  x
) )  e.  _V
2523, 19, 24fvmpt3i 5741 . . . . . . . . 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 2388 . . . . . . 7  |-  ( (
ph  /\  y  e.  V )  ->  (
( ( x  e.  V  |->  ( sqr `  (
x  .,  x )
) ) `  y
)  =  0  <->  ( sqr `  ( y  .,  y ) )  =  0 ) )
28 eqid 2380 . . . . . . . . . . . . . . 15  |-  ( Base `  F )  =  (
Base `  F )
29 phllvec 16776 . . . . . . . . . . . . . . . . 17  |-  ( W  e.  PreHil  ->  W  e.  LVec )
301, 29syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  W  e.  LVec )
3114lvecdrng 16097 . . . . . . . . . . . . . . . 16  |-  ( W  e.  LVec  ->  F  e.  DivRing )
3230, 31syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  e.  DivRing )
3328, 15, 32cphsubrglem 19004 . . . . . . . . . . . . . 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 3498 . . . . . . . . . . . . 13  |-  ( K  i^i  CC )  C_  CC
3634, 35syl6eqss 3334 . . . . . . . . . . . 12  |-  ( ph  ->  ( Base `  F
)  C_  CC )
3736adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  V )  ->  ( Base `  F )  C_  CC )
3814, 6, 5, 28ipcl 16780 . . . . . . . . . . . . 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 3285 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  V )  ->  (
y  .,  y )  e.  CC )
4241sqrcld 12159 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  V )  ->  ( sqr `  ( y  .,  y ) )  e.  CC )
43 sqeq0 11366 . . . . . . . . 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 12161 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  V )  ->  (
( sqr `  (
y  .,  y )
) ^ 2 )  =  ( y  .,  y ) )
462, 5, 14, 1, 15tchclm 19053 . . . . . . . . . . 11  |-  ( ph  ->  W  e. CMod )
4714clm0 18961 . . . . . . . . . . 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 2394 . . . . . . . 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 2380 . . . . . . . . 9  |-  ( 0g
`  F )  =  ( 0g `  F
)
5314, 6, 5, 52, 9ipeq0 16785 . . . . . . . 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 9040 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  K  /\  x  e.  RR  /\  0  <_  x ) )  ->  x  e.  CC )
6362sqrcld 12159 . . . . . . . . . . . . . 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 2447 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( x  e.  (
Base `  F )  <->  x  e.  ( K  i^i  CC ) ) )
67 recn 9006 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  x  e.  CC )
68 elin 3466 . . . . . . . . . . . . . . . . . . 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 2447 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( sqr `  x
)  e.  ( Base `  F )  <->  ( sqr `  x )  e.  ( K  i^i  CC ) ) )
78 elin 3466 . . . . . . . . . . . . 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 19056 . . . . . . 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 14789 . . . . . . . . . 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 6022 . . . . . . . . . . 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 5665 . . . . . . . . 9  |-  ( x  =  ( y (
-g `  W )
z )  ->  ( sqr `  ( x  .,  x ) )  =  ( sqr `  (
( y ( -g `  W ) z ) 
.,  ( y (
-g `  W )
z ) ) ) )
9493, 19, 24fvmpt3i 5741 . . . . . . . 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 6022 . . . . . . . . . . . 12  |-  ( ( x  =  z  /\  x  =  z )  ->  ( x  .,  x
)  =  ( z 
.,  z ) )
9796anidms 627 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
x  .,  x )  =  ( z  .,  z ) )
9897fveq2d 5665 . . . . . . . . . 10  |-  ( x  =  z  ->  ( sqr `  ( x  .,  x ) )  =  ( sqr `  (
z  .,  z )
) )
9998, 19, 24fvmpt3i 5741 . . . . . . . . 9  |-  ( z  e.  V  ->  (
( x  e.  V  |->  ( sqr `  (
x  .,  x )
) ) `  z
)  =  ( sqr `  ( z  .,  z
) ) )
10025, 99oveqan12d 6032 . . . . . . . 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 4176 . . . . . 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 18558 . . . . 5  |-  ( ph  ->  G  e. NrmGrp )
104 phllmod 16777 . . . . . 6  |-  ( G  e.  PreHil  ->  G  e.  LMod )
1054, 104syl 16 . . . . 5  |-  ( ph  ->  G  e.  LMod )
106 cnnrg 18679 . . . . . . 7  |-fld  e. NrmRing
10733simp3d 971 . . . . . . 7  |-  ( ph  ->  ( Base `  F
)  e.  (SubRing ` fld ) )
108 eqid 2380 . . . . . . . 8  |-  (flds  ( Base `  F
) )  =  (flds  ( Base `  F ) )
109108subrgnrg 18573 . . . . . . 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 2454 . . . . 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 2380 . . . . . . 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 19057 . . . . . 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 15887 . . . . . . . . 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 2380 . . . . . . . 8  |-  ( norm `  G )  =  (
norm `  G )
1262, 125, 5, 6tchnmval 19051 . . . . . . 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 5665 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
( norm `  F )  =  ( norm `  (flds  ( Base `  F ) ) ) )
129128fveq1d 5663 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
( ( norm `  F
) `  y )  =  ( ( norm `  (flds  (
Base `  F )
) ) `  y
) )
130 subrgsubg 15794 . . . . . . . . . . 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 18677 . . . . . . . . . 10  |-  abs  =  ( norm ` fld )
134 eqid 2380 . . . . . . . . . 10  |-  ( norm `  (flds  (
Base `  F )
) )  =  (
norm `  (flds  ( Base `  F
) ) )
135108, 133, 134subgnm2 18539 . . . . . . . . 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 2412 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
( ( norm `  F
) `  y )  =  ( abs `  y
) )
1382, 125, 5, 6tchnmval 19051 . . . . . . . 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 6031 . . . . . 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 2422 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  F
)  /\  z  e.  V ) )  -> 
( ( norm `  G
) `  ( y
( .s `  W
) z ) )  =  ( ( (
norm `  F ) `  y )  x.  (
( norm `  G ) `  z ) ) )
142141ralrimivva 2734 . . . 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 19042 . . . . 5  |-  V  =  ( Base `  G
)
1442, 117tchvsca 19046 . . . . 5  |-  ( .s
`  W )  =  ( .s `  G
)
1452, 14tchsca 19045 . . . . 5  |-  F  =  (Scalar `  G )
146 eqid 2380 . . . . 5  |-  ( norm `  F )  =  (
norm `  F )
147143, 125, 144, 145, 28, 146isnlm 18575 . . . 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 3466 . . . . . 6  |-  ( x  e.  ( ( Base `  F )  i^i  (
0 [,)  +oo ) )  <-> 
( x  e.  (
Base `  F )  /\  x  e.  (
0 [,)  +oo ) ) )
151 elrege0 10932 . . . . . . 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 2724 . . 3  |-  ( ph  ->  A. x  e.  ( ( Base `  F
)  i^i  ( 0 [,)  +oo ) ) ( sqr `  x )  e.  ( Base `  F
) )
156 sqrf 12087 . . . . 5  |-  sqr : CC
--> CC
157 ffun 5526 . . . . 5  |-  ( sqr
: CC --> CC  ->  Fun 
sqr )
158156, 157ax-mp 8 . . . 4  |-  Fun  sqr
159 inss1 3497 . . . . . 6  |-  ( (
Base `  F )  i^i  ( 0 [,)  +oo ) )  C_  ( Base `  F )
160159, 36syl5ss 3295 . . . . 5  |-  ( ph  ->  ( ( Base `  F
)  i^i  ( 0 [,)  +oo ) )  C_  CC )
161156fdmi 5529 . . . . 5  |-  dom  sqr  =  CC
162160, 161syl6sseqr 3331 . . . 4  |-  ( ph  ->  ( ( Base `  F
)  i^i  ( 0 [,)  +oo ) )  C_  dom  sqr )
163 funimass4 5709 . . . 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 2380 . . . . 5  |-  ( y  e.  V  |->  ( sqr `  ( y  .,  y
) ) )  =  ( y  e.  V  |->  ( sqr `  (
y  .,  y )
) )
16742, 166fmptd 5825 . . . 4  |-  ( ph  ->  ( y  e.  V  |->  ( sqr `  (
y  .,  y )
) ) : V --> CC )
1682, 5, 6tchval 19041 . . . . 5  |-  G  =  ( W toNrmGrp  ( y  e.  V  |->  ( sqr `  ( y  .,  y
) ) ) )
169 cnex 8997 . . . . 5  |-  CC  e.  _V
170168, 5, 169tngnm 18556 . . . 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 2385 . 2  |-  ( ph  ->  ( norm `  G
)  =  ( y  e.  V  |->  ( sqr `  ( y  .,  y
) ) ) )
1732, 6tchip 19047 . . 3  |-  .,  =  ( .i `  G )
174143, 173, 125, 145, 28iscph 18997 . 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 1717   A.wral 2642    i^i cin 3255    C_ wss 3256   class class class wbr 4146    e. cmpt 4200   dom cdm 4811   "cima 4814   Fun wfun 5381   -->wf 5383   ` cfv 5387  (class class class)co 6013   CCcc 8914   RRcr 8915   0cc0 8916    + caddc 8919    x. cmul 8921    +oocpnf 9043    <_ cle 9047   2c2 9974   [,)cico 10843   ^cexp 11302   sqrcsqr 11958   abscabs 11959   Basecbs 13389   ↾s cress 13390  Scalarcsca 13452   .scvsca 13453   .icip 13454   0gc0g 13643   Grpcgrp 14605   -gcsg 14608  SubGrpcsubg 14858   DivRingcdr 15755  SubRingcsubrg 15784   LModclmod 15870   LVecclvec 16094  ℂfldccnfld 16619   PreHilcphl 16771   normcnm 18488  NrmGrpcngp 18489  NrmRingcnrg 18491  NrmModcnlm 18492  CModcclm 18951   CPreHilccph 18993  toCHilctch 18994
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 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-rep 4254  ax-sep 4264  ax-nul 4272  ax-pow 4311  ax-pr 4337  ax-un 4634  ax-cnex 8972  ax-resscn 8973  ax-1cn 8974  ax-icn 8975  ax-addcl 8976  ax-addrcl 8977  ax-mulcl 8978  ax-mulrcl 8979  ax-mulcom 8980  ax-addass 8981  ax-mulass 8982  ax-distr 8983  ax-i2m1 8984  ax-1ne0 8985  ax-1rid 8986  ax-rnegex 8987  ax-rrecex 8988  ax-cnre 8989  ax-pre-lttri 8990  ax-pre-lttrn 8991  ax-pre-ltadd 8992  ax-pre-mulgt0 8993  ax-pre-sup 8994  ax-addf 8995  ax-mulf 8996
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 2235  df-mo 2236  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-nel 2546  df-ral 2647  df-rex 2648  df-reu 2649  df-rmo 2650  df-rab 2651  df-v 2894  df-sbc 3098  df-csb 3188  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-pss 3272  df-nul 3565  df-if 3676  df-pw 3737  df-sn 3756  df-pr 3757  df-tp 3758  df-op 3759  df-uni 3951  df-int 3986  df-iun 4030  df-br 4147  df-opab 4201  df-mpt 4202  df-tr 4237  df-eprel 4428  df-id 4432  df-po 4437  df-so 4438  df-fr 4475  df-we 4477  df-ord 4518  df-on 4519  df-lim 4520  df-suc 4521  df-om 4779  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5351  df-fun 5389  df-fn 5390  df-f 5391  df-f1 5392  df-fo 5393  df-f1o 5394  df-fv 5395  df-ov 6016  df-oprab 6017  df-mpt2 6018  df-1st 6281  df-2nd 6282  df-tpos 6408  df-riota 6478  df-recs 6562  df-rdg 6597  df-1o 6653  df-oadd 6657  df-er 6834  df-map 6949  df-en 7039  df-dom 7040  df-sdom 7041  df-fin 7042  df-sup 7374  df-pnf 9048  df-mnf 9049  df-xr 9050  df-ltxr 9051  df-le 9052  df-sub 9218  df-neg 9219  df-div 9603  df-nn 9926  df-2 9983  df-3 9984  df-4 9985  df-5 9986  df-6 9987  df-7 9988  df-8 9989  df-9 9990  df-10 9991  df-n0 10147  df-z 10208  df-dec 10308  df-uz 10414  df-q 10500  df-rp 10538  df-xneg 10635  df-xadd 10636  df-xmul 10637  df-ico 10847  df-fz 10969  df-seq 11244  df-exp 11303  df-cj 11824  df-re 11825  df-im 11826  df-sqr 11960  df-abs 11961  df-struct 13391  df-ndx 13392  df-slot 13393  df-base 13394  df-sets 13395  df-ress 13396  df-plusg 13462  df-mulr 13463  df-starv 13464  df-sca 13465  df-vsca 13466  df-ip 13467  df-tset 13468  df-ple 13469  df-ds 13471  df-unif 13472  df-rest 13570  df-topn 13571  df-topgen 13587  df-0g 13647  df-mnd 14610  df-mhm 14658  df-grp 14732  df-minusg 14733  df-sbg 14734  df-subg 14861  df-ghm 14924  df-cmn 15334  df-abl 15335  df-mgp 15569  df-rng 15583  df-cring 15584  df-ur 15585  df-oppr 15648  df-dvdsr 15666  df-unit 15667  df-invr 15697  df-dvr 15708  df-rnghom 15739  df-drng 15757  df-subrg 15786  df-abv 15825  df-staf 15853  df-srng 15854  df-lmod 15872  df-lmhm 16018  df-lvec 16095  df-sra 16164  df-rgmod 16165  df-xmet 16612  df-met 16613  df-bl 16614  df-mopn 16615  df-cnfld 16620  df-phl 16773  df-top 16879  df-bases 16881  df-topon 16882  df-topsp 16883  df-xms 18252  df-ms 18253  df-nm 18494  df-ngp 18495  df-tng 18496  df-nrg 18497  df-nlm 18498  df-clm 18952  df-cph 18995  df-tch 18996
  Copyright terms: Public domain W3C validator