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

Definition df-obs 19255
Description: Define the set of all orthonormal bases for a pre-Hilbert space. An orthonormal basis is a set of mutually orthogonal vectors with norm 1 and such that the linear span is dense in the whole space. (As this is an "algebraic" definition, before we have topology available, we express this denseness by saying that the double orthocomplement is the whole space, or equivalently, the single orthocomplement is trivial.) (Contributed by Mario Carneiro, 23-Oct-2015.)
Assertion
Ref Expression
df-obs  |- OBasis  =  ( h  e.  PreHil  |->  { b  e.  ~P ( Base `  h )  |  ( A. x  e.  b 
A. y  e.  b  ( x ( .i
`  h ) y )  =  if ( x  =  y ,  ( 1r `  (Scalar `  h ) ) ,  ( 0g `  (Scalar `  h ) ) )  /\  ( ( ocv `  h ) `  b
)  =  { ( 0g `  h ) } ) } )
Distinct variable group:    h, b, x, y

Detailed syntax breakdown of Definition df-obs
StepHypRef Expression
1 cobs 19252 . 2  class OBasis
2 vh . . 3  setvar  h
3 cphl 19178 . . 3  class  PreHil
4 vx . . . . . . . . . 10  setvar  x
54cv 1436 . . . . . . . . 9  class  x
6 vy . . . . . . . . . 10  setvar  y
76cv 1436 . . . . . . . . 9  class  y
82cv 1436 . . . . . . . . . 10  class  h
9 cip 15183 . . . . . . . . . 10  class  .i
108, 9cfv 5598 . . . . . . . . 9  class  ( .i
`  h )
115, 7, 10co 6302 . . . . . . . 8  class  ( x ( .i `  h
) y )
124, 6weq 1780 . . . . . . . . 9  wff  x  =  y
13 csca 15181 . . . . . . . . . . 11  class Scalar
148, 13cfv 5598 . . . . . . . . . 10  class  (Scalar `  h )
15 cur 17723 . . . . . . . . . 10  class  1r
1614, 15cfv 5598 . . . . . . . . 9  class  ( 1r
`  (Scalar `  h )
)
17 c0g 15326 . . . . . . . . . 10  class  0g
1814, 17cfv 5598 . . . . . . . . 9  class  ( 0g
`  (Scalar `  h )
)
1912, 16, 18cif 3909 . . . . . . . 8  class  if ( x  =  y ,  ( 1r `  (Scalar `  h ) ) ,  ( 0g `  (Scalar `  h ) ) )
2011, 19wceq 1437 . . . . . . 7  wff  ( x ( .i `  h
) y )  =  if ( x  =  y ,  ( 1r
`  (Scalar `  h )
) ,  ( 0g
`  (Scalar `  h )
) )
21 vb . . . . . . . 8  setvar  b
2221cv 1436 . . . . . . 7  class  b
2320, 6, 22wral 2775 . . . . . 6  wff  A. y  e.  b  ( x
( .i `  h
) y )  =  if ( x  =  y ,  ( 1r
`  (Scalar `  h )
) ,  ( 0g
`  (Scalar `  h )
) )
2423, 4, 22wral 2775 . . . . 5  wff  A. x  e.  b  A. y  e.  b  ( x
( .i `  h
) y )  =  if ( x  =  y ,  ( 1r
`  (Scalar `  h )
) ,  ( 0g
`  (Scalar `  h )
) )
25 cocv 19210 . . . . . . . 8  class  ocv
268, 25cfv 5598 . . . . . . 7  class  ( ocv `  h )
2722, 26cfv 5598 . . . . . 6  class  ( ( ocv `  h ) `
 b )
288, 17cfv 5598 . . . . . . 7  class  ( 0g
`  h )
2928csn 3996 . . . . . 6  class  { ( 0g `  h ) }
3027, 29wceq 1437 . . . . 5  wff  ( ( ocv `  h ) `
 b )  =  { ( 0g `  h ) }
3124, 30wa 370 . . . 4  wff  ( A. x  e.  b  A. y  e.  b  (
x ( .i `  h ) y )  =  if ( x  =  y ,  ( 1r `  (Scalar `  h ) ) ,  ( 0g `  (Scalar `  h ) ) )  /\  ( ( ocv `  h ) `  b
)  =  { ( 0g `  h ) } )
32 cbs 15109 . . . . . 6  class  Base
338, 32cfv 5598 . . . . 5  class  ( Base `  h )
3433cpw 3979 . . . 4  class  ~P ( Base `  h )
3531, 21, 34crab 2779 . . 3  class  { b  e.  ~P ( Base `  h )  |  ( A. x  e.  b 
A. y  e.  b  ( x ( .i
`  h ) y )  =  if ( x  =  y ,  ( 1r `  (Scalar `  h ) ) ,  ( 0g `  (Scalar `  h ) ) )  /\  ( ( ocv `  h ) `  b
)  =  { ( 0g `  h ) } ) }
362, 3, 35cmpt 4479 . 2  class  ( h  e.  PreHil  |->  { b  e. 
~P ( Base `  h
)  |  ( A. x  e.  b  A. y  e.  b  (
x ( .i `  h ) y )  =  if ( x  =  y ,  ( 1r `  (Scalar `  h ) ) ,  ( 0g `  (Scalar `  h ) ) )  /\  ( ( ocv `  h ) `  b
)  =  { ( 0g `  h ) } ) } )
371, 36wceq 1437 1  wff OBasis  =  ( h  e.  PreHil  |->  { b  e.  ~P ( Base `  h )  |  ( A. x  e.  b 
A. y  e.  b  ( x ( .i
`  h ) y )  =  if ( x  =  y ,  ( 1r `  (Scalar `  h ) ) ,  ( 0g `  (Scalar `  h ) ) )  /\  ( ( ocv `  h ) `  b
)  =  { ( 0g `  h ) } ) } )
Colors of variables: wff setvar class
This definition is referenced by:  isobs  19270
  Copyright terms: Public domain W3C validator