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 ) ) } ) )