MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ocv Unicode version

Definition df-ocv 16563
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
StepHypRef Expression
1 cocv 16560 . 2  class  ocv
2 vh . . 3  set  h
3 cvv 2788 . . 3  class  _V
4 vs . . . 4  set  s
52cv 1622 . . . . . 6  class  h
6 cbs 13148 . . . . . 6  class  Base
75, 6cfv 5255 . . . . 5  class  ( Base `  h )
87cpw 3625 . . . 4  class  ~P ( Base `  h )
9 vx . . . . . . . . 9  set  x
109cv 1622 . . . . . . . 8  class  x
11 vy . . . . . . . . 9  set  y
1211cv 1622 . . . . . . . 8  class  y
13 cip 13213 . . . . . . . . 9  class  .i
145, 13cfv 5255 . . . . . . . 8  class  ( .i
`  h )
1510, 12, 14co 5858 . . . . . . 7  class  ( x ( .i `  h
) y )
16 csca 13211 . . . . . . . . 9  class Scalar
175, 16cfv 5255 . . . . . . . 8  class  (Scalar `  h )
18 c0g 13400 . . . . . . . 8  class  0g
1917, 18cfv 5255 . . . . . . 7  class  ( 0g
`  (Scalar `  h )
)
2015, 19wceq 1623 . . . . . 6  wff  ( x ( .i `  h
) y )  =  ( 0g `  (Scalar `  h ) )
214cv 1622 . . . . . 6  class  s
2220, 11, 21wral 2543 . . . . 5  wff  A. y  e.  s  ( x
( .i `  h
) y )  =  ( 0g `  (Scalar `  h ) )
2322, 9, 7crab 2547 . . . 4  class  { x  e.  ( Base `  h
)  |  A. y  e.  s  ( x
( .i `  h
) y )  =  ( 0g `  (Scalar `  h ) ) }
244, 8, 23cmpt 4077 . . 3  class  ( s  e.  ~P ( Base `  h )  |->  { x  e.  ( Base `  h
)  |  A. y  e.  s  ( x
( .i `  h
) y )  =  ( 0g `  (Scalar `  h ) ) } )
252, 3, 24cmpt 4077 . 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 ) ) } ) )
261, 25wceq 1623 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 )
) } ) )
Colors of variables: wff set class
This definition is referenced by:  ocvfval  16566
  Copyright terms: Public domain W3C validator