Definition df-ocv 19161

Description: Define orthocomplement of a subspace. (Contributed by NM, 7-Oct-2011.)

Assertion

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

Distinct variable group:   h, s, x, y

Detailed syntax breakdown of Definition df-ocv

Step	Hyp	Ref	Expression
1		cocv 19158	. 2 class ocv
2		vh	. . 3 setvar h
3		cvv 3087	. . 3 class _V
4		vs	. . . 4 setvar s
5	2	cv 1436	. . . . . 6 class h
6		cbs 15084	. . . . . 6 class Base
7	5, 6	cfv 5601	. . . . 5 class ( Base ` h )
8	7	cpw 3985	. . . 4 class ~P ( Base ` h )
9		vx	. . . . . . . . 9 setvar x
10	9	cv 1436	. . . . . . . 8 class x
11		vy	. . . . . . . . 9 setvar y
12	11	cv 1436	. . . . . . . 8 class y
13		cip 15158	. . . . . . . . 9 class .i
14	5, 13	cfv 5601	. . . . . . . 8 class ( .i ` h )
15	10, 12, 14	co 6305	. . . . . . 7 class ( x ( .i ` h ) y )
16		csca 15156	. . . . . . . . 9 class Scalar
17	5, 16	cfv 5601	. . . . . . . 8 class (Scalar ` h )
18		c0g 15301	. . . . . . . 8 class 0g
19	17, 18	cfv 5601	. . . . . . 7 class ( 0g ` (Scalar ` h ) )
20	15, 19	wceq 1437	. . . . . 6 wff ( x ( .i ` h ) y ) = ( 0g ` (Scalar ` h ) )
21	4	cv 1436	. . . . . 6 class s
22	20, 11, 21	wral 2782	. . . . 5 wff A. y e. s ( x ( .i ` h ) y ) = ( 0g ` (Scalar ` h ) )
23	22, 9, 7	crab 2786	. . . 4 class { x e. ( Base ` h ) | A. y e. s ( x ( .i ` h ) y ) = ( 0g ` (Scalar ` h ) ) }
24	4, 8, 23	cmpt 4484	. . 3 class ( s e. ~P ( Base ` h ) |-> { x e. ( Base ` h ) | A. y e. s ( x ( .i ` h ) y ) = ( 0g ` (Scalar ` h ) ) } )
25	2, 3, 24	cmpt 4484	. 2 class ( h e. _V |-> ( s e. ~P ( Base ` h ) |-> { x e. ( Base ` h ) | A. y e. s ( x ( .i ` h ) y ) = ( 0g ` (Scalar ` h ) ) } ) )
26	1, 25	wceq 1437	1 wff ocv = ( h e. _V |-> ( s e. ~P ( Base ` h ) |-> { x e. ( Base ` h ) | A. y e. s ( x ( .i ` h ) y ) = ( 0g ` (Scalar ` h ) ) } ) )

This definition is referenced by:  ocvfval  19164