Definition df-ocv 18563

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 18560	. 2 class ocv
2		vh	. . 3 setvar h
3		cvv 3118	. . 3 class _V
4		vs	. . . 4 setvar s
5	2	cv 1378	. . . . . 6 class h
6		cbs 14507	. . . . . 6 class Base
7	5, 6	cfv 5594	. . . . 5 class ( Base ` h )
8	7	cpw 4016	. . . 4 class ~P ( Base ` h )
9		vx	. . . . . . . . 9 setvar x
10	9	cv 1378	. . . . . . . 8 class x
11		vy	. . . . . . . . 9 setvar y
12	11	cv 1378	. . . . . . . 8 class y
13		cip 14577	. . . . . . . . 9 class .i
14	5, 13	cfv 5594	. . . . . . . 8 class ( .i ` h )
15	10, 12, 14	co 6295	. . . . . . 7 class ( x ( .i ` h ) y )
16		csca 14575	. . . . . . . . 9 class Scalar
17	5, 16	cfv 5594	. . . . . . . 8 class (Scalar ` h )
18		c0g 14712	. . . . . . . 8 class 0g
19	17, 18	cfv 5594	. . . . . . 7 class ( 0g ` (Scalar ` h ) )
20	15, 19	wceq 1379	. . . . . 6 wff ( x ( .i ` h ) y ) = ( 0g ` (Scalar ` h ) )
21	4	cv 1378	. . . . . 6 class s
22	20, 11, 21	wral 2817	. . . . 5 wff A. y e. s ( x ( .i ` h ) y ) = ( 0g ` (Scalar ` h ) )
23	22, 9, 7	crab 2821	. . . 4 class { x e. ( Base ` h ) | A. y e. s ( x ( .i ` h ) y ) = ( 0g ` (Scalar ` h ) ) }
24	4, 8, 23	cmpt 4511	. . 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 4511	. 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 1379	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  18566