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

Definition df-ocv 16579
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 16576 . 2  class  ocv
2 vh . . 3  set  h
3 cvv 2801 . . 3  class  _V
4 vs . . . 4  set  s
52cv 1631 . . . . . 6  class  h
6 cbs 13164 . . . . . 6  class  Base
75, 6cfv 5271 . . . . 5  class  ( Base `  h )
87cpw 3638 . . . 4  class  ~P ( Base `  h )
9 vx . . . . . . . . 9  set  x
109cv 1631 . . . . . . . 8  class  x
11 vy . . . . . . . . 9  set  y
1211cv 1631 . . . . . . . 8  class  y
13 cip 13229 . . . . . . . . 9  class  .i
145, 13cfv 5271 . . . . . . . 8  class  ( .i
`  h )
1510, 12, 14co 5874 . . . . . . 7  class  ( x ( .i `  h
) y )
16 csca 13227 . . . . . . . . 9  class Scalar
175, 16cfv 5271 . . . . . . . 8  class  (Scalar `  h )
18 c0g 13416 . . . . . . . 8  class  0g
1917, 18cfv 5271 . . . . . . 7  class  ( 0g
`  (Scalar `  h )
)
2015, 19wceq 1632 . . . . . 6  wff  ( x ( .i `  h
) y )  =  ( 0g `  (Scalar `  h ) )
214cv 1631 . . . . . 6  class  s
2220, 11, 21wral 2556 . . . . 5  wff  A. y  e.  s  ( x
( .i `  h
) y )  =  ( 0g `  (Scalar `  h ) )
2322, 9, 7crab 2560 . . . 4  class  { x  e.  ( Base `  h
)  |  A. y  e.  s  ( x
( .i `  h
) y )  =  ( 0g `  (Scalar `  h ) ) }
244, 8, 23cmpt 4093 . . 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 4093 . 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 1632 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  16582
  Copyright terms: Public domain W3C validator