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

Definition df-obs 16605
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 16602 . 2  class OBasis
2 vh . . 3  set  h
3 cphl 16528 . . 3  class  PreHil
4 vx . . . . . . . . . 10  set  x
54cv 1622 . . . . . . . . 9  class  x
6 vy . . . . . . . . . 10  set  y
76cv 1622 . . . . . . . . 9  class  y
82cv 1622 . . . . . . . . . 10  class  h
9 cip 13213 . . . . . . . . . 10  class  .i
108, 9cfv 5255 . . . . . . . . 9  class  ( .i
`  h )
115, 7, 10co 5858 . . . . . . . 8  class  ( x ( .i `  h
) y )
124, 6weq 1624 . . . . . . . . 9  wff  x  =  y
13 csca 13211 . . . . . . . . . . 11  class Scalar
148, 13cfv 5255 . . . . . . . . . 10  class  (Scalar `  h )
15 cur 15339 . . . . . . . . . 10  class  1r
1614, 15cfv 5255 . . . . . . . . 9  class  ( 1r
`  (Scalar `  h )
)
17 c0g 13400 . . . . . . . . . 10  class  0g
1814, 17cfv 5255 . . . . . . . . 9  class  ( 0g
`  (Scalar `  h )
)
1912, 16, 18cif 3565 . . . . . . . 8  class  if ( x  =  y ,  ( 1r `  (Scalar `  h ) ) ,  ( 0g `  (Scalar `  h ) ) )
2011, 19wceq 1623 . . . . . . 7  wff  ( x ( .i `  h
) y )  =  if ( x  =  y ,  ( 1r
`  (Scalar `  h )
) ,  ( 0g
`  (Scalar `  h )
) )
21 vb . . . . . . . 8  set  b
2221cv 1622 . . . . . . 7  class  b
2320, 6, 22wral 2543 . . . . . 6  wff  A. y  e.  b  ( x
( .i `  h
) y )  =  if ( x  =  y ,  ( 1r
`  (Scalar `  h )
) ,  ( 0g
`  (Scalar `  h )
) )
2423, 4, 22wral 2543 . . . . 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 16560 . . . . . . . 8  class  ocv
268, 25cfv 5255 . . . . . . 7  class  ( ocv `  h )
2722, 26cfv 5255 . . . . . 6  class  ( ( ocv `  h ) `
 b )
288, 17cfv 5255 . . . . . . 7  class  ( 0g
`  h )
2928csn 3640 . . . . . 6  class  { ( 0g `  h ) }
3027, 29wceq 1623 . . . . 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 13148 . . . . . 6  class  Base
338, 32cfv 5255 . . . . 5  class  ( Base `  h )
3433cpw 3625 . . . 4  class  ~P ( Base `  h )
3531, 21, 34crab 2547 . . 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 4077 . 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 1623 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  16620
  Copyright terms: Public domain W3C validator