This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ocv

Description: Define the orthocomplement function in a given set (which usually is a pre-Hilbert space): it associates with a subset its orthogonal subset (which in the case of a closed linear subspace is its orthocomplement). (Contributed by NM, 7-Oct-2011)

Ref Expression
Assertion df-ocv 
|- ocv = ( h e. _V |-> ( s e. ~P ( Base ` h ) |-> { x e. ( Base ` h ) | A. y e. s ( x ( .i ` h ) y ) = ( 0g ` ( Scalar ` h ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cocv 
 |-  ocv
1 vh 
 |-  h
2 cvv 
 |-  _V
3 vs 
 |-  s
4 cbs 
 |-  Base
5 1 cv 
 |-  h
6 5 4 cfv 
 |-  ( Base ` h )
7 6 cpw 
 |-  ~P ( Base ` h )
8 vx 
 |-  x
9 vy 
 |-  y
10 3 cv 
 |-  s
11 8 cv 
 |-  x
12 cip 
 |-  .i
13 5 12 cfv 
 |-  ( .i ` h )
14 9 cv 
 |-  y
15 11 14 13 co 
 |-  ( x ( .i ` h ) y )
16 c0g 
 |-  0g
17 csca 
 |-  Scalar
18 5 17 cfv 
 |-  ( Scalar ` h )
19 18 16 cfv 
 |-  ( 0g ` ( Scalar ` h ) )
20 15 19 wceq 
 |-  ( x ( .i ` h ) y ) = ( 0g ` ( Scalar ` h ) )
21 20 9 10 wral 
 |-  A. y e. s ( x ( .i ` h ) y ) = ( 0g ` ( Scalar ` h ) )
22 21 8 6 crab 
 |-  { x e. ( Base ` h ) | A. y e. s ( x ( .i ` h ) y ) = ( 0g ` ( Scalar ` h ) ) }
23 3 7 22 cmpt 
 |-  ( s e. ~P ( Base ` h ) |-> { x e. ( Base ` h ) | A. y e. s ( x ( .i ` h ) y ) = ( 0g ` ( Scalar ` h ) ) } )
24 1 2 23 cmpt 
 |-  ( h e. _V |-> ( s e. ~P ( Base ` h ) |-> { x e. ( Base ` h ) | A. y e. s ( x ( .i ` h ) y ) = ( 0g ` ( Scalar ` h ) ) } ) )
25 0 24 wceq 
 |-  ocv = ( h e. _V |-> ( s e. ~P ( Base ` h ) |-> { x e. ( Base ` h ) | A. y e. s ( x ( .i ` h ) y ) = ( 0g ` ( Scalar ` h ) ) } ) )