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

Definition df-phl 16530
Description: Define class all generalized pre-Hilbert (inner product) spaces. (Contributed by NM, 22-Sep-2011.)
Assertion
Ref Expression
df-phl  |-  PreHil  =  {
g  e.  LVec  |  [. ( Base `  g )  /  v ]. [. ( .i `  g )  /  h ]. [. (Scalar `  g )  /  f ]. ( f  e.  *Ring  /\ 
A. x  e.  v  ( ( y  e.  v  |->  ( y h x ) )  e.  ( g LMHom  (ringLMod `  f
) )  /\  (
( x h x )  =  ( 0g
`  f )  ->  x  =  ( 0g `  g ) )  /\  A. y  e.  v  ( ( * r `  f ) `  (
x h y ) )  =  ( y h x ) ) ) }
Distinct variable group:    f, g, h, v, x, y

Detailed syntax breakdown of Definition df-phl
StepHypRef Expression
1 cphl 16528 . 2  class  PreHil
2 vf . . . . . . . . 9  set  f
32cv 1622 . . . . . . . 8  class  f
4 csr 15609 . . . . . . . 8  class  *Ring
53, 4wcel 1684 . . . . . . 7  wff  f  e.  *Ring
6 vy . . . . . . . . . . 11  set  y
7 vv . . . . . . . . . . . 12  set  v
87cv 1622 . . . . . . . . . . 11  class  v
96cv 1622 . . . . . . . . . . . 12  class  y
10 vx . . . . . . . . . . . . 13  set  x
1110cv 1622 . . . . . . . . . . . 12  class  x
12 vh . . . . . . . . . . . . 13  set  h
1312cv 1622 . . . . . . . . . . . 12  class  h
149, 11, 13co 5858 . . . . . . . . . . 11  class  ( y h x )
156, 8, 14cmpt 4077 . . . . . . . . . 10  class  ( y  e.  v  |->  ( y h x ) )
16 vg . . . . . . . . . . . 12  set  g
1716cv 1622 . . . . . . . . . . 11  class  g
18 crglmod 15922 . . . . . . . . . . . 12  class ringLMod
193, 18cfv 5255 . . . . . . . . . . 11  class  (ringLMod `  f
)
20 clmhm 15776 . . . . . . . . . . 11  class LMHom
2117, 19, 20co 5858 . . . . . . . . . 10  class  ( g LMHom 
(ringLMod `  f ) )
2215, 21wcel 1684 . . . . . . . . 9  wff  ( y  e.  v  |->  ( y h x ) )  e.  ( g LMHom  (ringLMod `  f ) )
2311, 11, 13co 5858 . . . . . . . . . . 11  class  ( x h x )
24 c0g 13400 . . . . . . . . . . . 12  class  0g
253, 24cfv 5255 . . . . . . . . . . 11  class  ( 0g
`  f )
2623, 25wceq 1623 . . . . . . . . . 10  wff  ( x h x )  =  ( 0g `  f
)
2717, 24cfv 5255 . . . . . . . . . . 11  class  ( 0g
`  g )
2811, 27wceq 1623 . . . . . . . . . 10  wff  x  =  ( 0g `  g
)
2926, 28wi 4 . . . . . . . . 9  wff  ( ( x h x )  =  ( 0g `  f )  ->  x  =  ( 0g `  g ) )
3011, 9, 13co 5858 . . . . . . . . . . . 12  class  ( x h y )
31 cstv 13210 . . . . . . . . . . . . 13  class  * r
323, 31cfv 5255 . . . . . . . . . . . 12  class  ( * r `  f )
3330, 32cfv 5255 . . . . . . . . . . 11  class  ( ( * r `  f
) `  ( x h y ) )
3433, 14wceq 1623 . . . . . . . . . 10  wff  ( ( * r `  f
) `  ( x h y ) )  =  ( y h x )
3534, 6, 8wral 2543 . . . . . . . . 9  wff  A. y  e.  v  ( (
* r `  f
) `  ( x h y ) )  =  ( y h x )
3622, 29, 35w3a 934 . . . . . . . 8  wff  ( ( y  e.  v  |->  ( y h x ) )  e.  ( g LMHom 
(ringLMod `  f ) )  /\  ( ( x h x )  =  ( 0g `  f
)  ->  x  =  ( 0g `  g ) )  /\  A. y  e.  v  ( (
* r `  f
) `  ( x h y ) )  =  ( y h x ) )
3736, 10, 8wral 2543 . . . . . . 7  wff  A. x  e.  v  ( (
y  e.  v  |->  ( y h x ) )  e.  ( g LMHom 
(ringLMod `  f ) )  /\  ( ( x h x )  =  ( 0g `  f
)  ->  x  =  ( 0g `  g ) )  /\  A. y  e.  v  ( (
* r `  f
) `  ( x h y ) )  =  ( y h x ) )
385, 37wa 358 . . . . . 6  wff  ( f  e.  *Ring  /\  A. x  e.  v  ( (
y  e.  v  |->  ( y h x ) )  e.  ( g LMHom 
(ringLMod `  f ) )  /\  ( ( x h x )  =  ( 0g `  f
)  ->  x  =  ( 0g `  g ) )  /\  A. y  e.  v  ( (
* r `  f
) `  ( x h y ) )  =  ( y h x ) ) )
39 csca 13211 . . . . . . 7  class Scalar
4017, 39cfv 5255 . . . . . 6  class  (Scalar `  g )
4138, 2, 40wsbc 2991 . . . . 5  wff  [. (Scalar `  g )  /  f ]. ( f  e.  *Ring  /\ 
A. x  e.  v  ( ( y  e.  v  |->  ( y h x ) )  e.  ( g LMHom  (ringLMod `  f
) )  /\  (
( x h x )  =  ( 0g
`  f )  ->  x  =  ( 0g `  g ) )  /\  A. y  e.  v  ( ( * r `  f ) `  (
x h y ) )  =  ( y h x ) ) )
42 cip 13213 . . . . . 6  class  .i
4317, 42cfv 5255 . . . . 5  class  ( .i
`  g )
4441, 12, 43wsbc 2991 . . . 4  wff  [. ( .i `  g )  /  h ]. [. (Scalar `  g )  /  f ]. ( f  e.  *Ring  /\ 
A. x  e.  v  ( ( y  e.  v  |->  ( y h x ) )  e.  ( g LMHom  (ringLMod `  f
) )  /\  (
( x h x )  =  ( 0g
`  f )  ->  x  =  ( 0g `  g ) )  /\  A. y  e.  v  ( ( * r `  f ) `  (
x h y ) )  =  ( y h x ) ) )
45 cbs 13148 . . . . 5  class  Base
4617, 45cfv 5255 . . . 4  class  ( Base `  g )
4744, 7, 46wsbc 2991 . . 3  wff  [. ( Base `  g )  / 
v ]. [. ( .i
`  g )  /  h ]. [. (Scalar `  g )  /  f ]. ( f  e.  *Ring  /\ 
A. x  e.  v  ( ( y  e.  v  |->  ( y h x ) )  e.  ( g LMHom  (ringLMod `  f
) )  /\  (
( x h x )  =  ( 0g
`  f )  ->  x  =  ( 0g `  g ) )  /\  A. y  e.  v  ( ( * r `  f ) `  (
x h y ) )  =  ( y h x ) ) )
48 clvec 15855 . . 3  class  LVec
4947, 16, 48crab 2547 . 2  class  { g  e.  LVec  |  [. ( Base `  g )  / 
v ]. [. ( .i
`  g )  /  h ]. [. (Scalar `  g )  /  f ]. ( f  e.  *Ring  /\ 
A. x  e.  v  ( ( y  e.  v  |->  ( y h x ) )  e.  ( g LMHom  (ringLMod `  f
) )  /\  (
( x h x )  =  ( 0g
`  f )  ->  x  =  ( 0g `  g ) )  /\  A. y  e.  v  ( ( * r `  f ) `  (
x h y ) )  =  ( y h x ) ) ) }
501, 49wceq 1623 1  wff  PreHil  =  {
g  e.  LVec  |  [. ( Base `  g )  /  v ]. [. ( .i `  g )  /  h ]. [. (Scalar `  g )  /  f ]. ( f  e.  *Ring  /\ 
A. x  e.  v  ( ( y  e.  v  |->  ( y h x ) )  e.  ( g LMHom  (ringLMod `  f
) )  /\  (
( x h x )  =  ( 0g
`  f )  ->  x  =  ( 0g `  g ) )  /\  A. y  e.  v  ( ( * r `  f ) `  (
x h y ) )  =  ( y h x ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  isphl  16532
  Copyright terms: Public domain W3C validator