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

Definition df-obs 16934
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 16931 . 2  class OBasis
2 vh . . 3  set  h
3 cphl 16857 . . 3  class  PreHil
4 vx . . . . . . . . . 10  set  x
54cv 1652 . . . . . . . . 9  class  x
6 vy . . . . . . . . . 10  set  y
76cv 1652 . . . . . . . . 9  class  y
82cv 1652 . . . . . . . . . 10  class  h
9 cip 13536 . . . . . . . . . 10  class  .i
108, 9cfv 5456 . . . . . . . . 9  class  ( .i
`  h )
115, 7, 10co 6083 . . . . . . . 8  class  ( x ( .i `  h
) y )
124, 6weq 1654 . . . . . . . . 9  wff  x  =  y
13 csca 13534 . . . . . . . . . . 11  class Scalar
148, 13cfv 5456 . . . . . . . . . 10  class  (Scalar `  h )
15 cur 15664 . . . . . . . . . 10  class  1r
1614, 15cfv 5456 . . . . . . . . 9  class  ( 1r
`  (Scalar `  h )
)
17 c0g 13725 . . . . . . . . . 10  class  0g
1814, 17cfv 5456 . . . . . . . . 9  class  ( 0g
`  (Scalar `  h )
)
1912, 16, 18cif 3741 . . . . . . . 8  class  if ( x  =  y ,  ( 1r `  (Scalar `  h ) ) ,  ( 0g `  (Scalar `  h ) ) )
2011, 19wceq 1653 . . . . . . 7  wff  ( x ( .i `  h
) y )  =  if ( x  =  y ,  ( 1r
`  (Scalar `  h )
) ,  ( 0g
`  (Scalar `  h )
) )
21 vb . . . . . . . 8  set  b
2221cv 1652 . . . . . . 7  class  b
2320, 6, 22wral 2707 . . . . . 6  wff  A. y  e.  b  ( x
( .i `  h
) y )  =  if ( x  =  y ,  ( 1r
`  (Scalar `  h )
) ,  ( 0g
`  (Scalar `  h )
) )
2423, 4, 22wral 2707 . . . . 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 16889 . . . . . . . 8  class  ocv
268, 25cfv 5456 . . . . . . 7  class  ( ocv `  h )
2722, 26cfv 5456 . . . . . 6  class  ( ( ocv `  h ) `
 b )
288, 17cfv 5456 . . . . . . 7  class  ( 0g
`  h )
2928csn 3816 . . . . . 6  class  { ( 0g `  h ) }
3027, 29wceq 1653 . . . . 5  wff  ( ( ocv `  h ) `
 b )  =  { ( 0g `  h ) }
3124, 30wa 360 . . . 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 13471 . . . . . 6  class  Base
338, 32cfv 5456 . . . . 5  class  ( Base `  h )
3433cpw 3801 . . . 4  class  ~P ( Base `  h )
3531, 21, 34crab 2711 . . 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 4268 . 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 1653 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  16949
  Copyright terms: Public domain W3C validator