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

Definition df-obs 16661
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 16658 . 2  class OBasis
2 vh . . 3  set  h
3 cphl 16584 . . 3  class  PreHil
4 vx . . . . . . . . . 10  set  x
54cv 1632 . . . . . . . . 9  class  x
6 vy . . . . . . . . . 10  set  y
76cv 1632 . . . . . . . . 9  class  y
82cv 1632 . . . . . . . . . 10  class  h
9 cip 13260 . . . . . . . . . 10  class  .i
108, 9cfv 5292 . . . . . . . . 9  class  ( .i
`  h )
115, 7, 10co 5900 . . . . . . . 8  class  ( x ( .i `  h
) y )
124, 6weq 1634 . . . . . . . . 9  wff  x  =  y
13 csca 13258 . . . . . . . . . . 11  class Scalar
148, 13cfv 5292 . . . . . . . . . 10  class  (Scalar `  h )
15 cur 15388 . . . . . . . . . 10  class  1r
1614, 15cfv 5292 . . . . . . . . 9  class  ( 1r
`  (Scalar `  h )
)
17 c0g 13449 . . . . . . . . . 10  class  0g
1814, 17cfv 5292 . . . . . . . . 9  class  ( 0g
`  (Scalar `  h )
)
1912, 16, 18cif 3599 . . . . . . . 8  class  if ( x  =  y ,  ( 1r `  (Scalar `  h ) ) ,  ( 0g `  (Scalar `  h ) ) )
2011, 19wceq 1633 . . . . . . 7  wff  ( x ( .i `  h
) y )  =  if ( x  =  y ,  ( 1r
`  (Scalar `  h )
) ,  ( 0g
`  (Scalar `  h )
) )
21 vb . . . . . . . 8  set  b
2221cv 1632 . . . . . . 7  class  b
2320, 6, 22wral 2577 . . . . . 6  wff  A. y  e.  b  ( x
( .i `  h
) y )  =  if ( x  =  y ,  ( 1r
`  (Scalar `  h )
) ,  ( 0g
`  (Scalar `  h )
) )
2423, 4, 22wral 2577 . . . . 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 16616 . . . . . . . 8  class  ocv
268, 25cfv 5292 . . . . . . 7  class  ( ocv `  h )
2722, 26cfv 5292 . . . . . 6  class  ( ( ocv `  h ) `
 b )
288, 17cfv 5292 . . . . . . 7  class  ( 0g
`  h )
2928csn 3674 . . . . . 6  class  { ( 0g `  h ) }
3027, 29wceq 1633 . . . . 5  wff  ( ( ocv `  h ) `
 b )  =  { ( 0g `  h ) }
3124, 30wa 358 . . . 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 13195 . . . . . 6  class  Base
338, 32cfv 5292 . . . . 5  class  ( Base `  h )
3433cpw 3659 . . . 4  class  ~P ( Base `  h )
3531, 21, 34crab 2581 . . 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 4114 . 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 1633 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 set class
This definition is referenced by:  isobs  16676
  Copyright terms: Public domain W3C validator