Definition df-ocv 20007

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 20004	. 2 class ocv
2		vh	. . 3 setvar h
3		cvv 3200	. . 3 class _V
4		vs	. . . 4 setvar s
5	2	cv 1482	. . . . . 6 class h
6		cbs 15857	. . . . . 6 class Base
7	5, 6	cfv 5888	. . . . 5 class ( Base ` h )
8	7	cpw 4158	. . . 4 class ~P ( Base ` h )
9		vx	. . . . . . . . 9 setvar x
10	9	cv 1482	. . . . . . . 8 class x
11		vy	. . . . . . . . 9 setvar y
12	11	cv 1482	. . . . . . . 8 class y
13		cip 15946	. . . . . . . . 9 class .i
14	5, 13	cfv 5888	. . . . . . . 8 class ( .i ` h )
15	10, 12, 14	co 6650	. . . . . . 7 class ( x ( .i ` h ) y )
16		csca 15944	. . . . . . . . 9 class Scalar
17	5, 16	cfv 5888	. . . . . . . 8 class (Scalar ` h )
18		c0g 16100	. . . . . . . 8 class 0g
19	17, 18	cfv 5888	. . . . . . 7 class ( 0g ` (Scalar ` h ) )
20	15, 19	wceq 1483	. . . . . 6 wff ( x ( .i ` h ) y ) = ( 0g ` (Scalar ` h ) )
21	4	cv 1482	. . . . . 6 class s
22	20, 11, 21	wral 2912	. . . . 5 wff A. y e. s ( x ( .i ` h ) y ) = ( 0g ` (Scalar ` h ) )
23	22, 9, 7	crab 2916	. . . 4 class { x e. ( Base ` h ) | A. y e. s ( x ( .i ` h ) y ) = ( 0g ` (Scalar ` h ) ) }
24	4, 8, 23	cmpt 4729	. . 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 4729	. 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 1483	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  20010