Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-doch Unicode version

Definition df-doch 32160
Description: Define subspace orthocomplement for  DVecH vector space. Temporarily, we are using the range of the isomorphism instead of the set of closed subspaces. Later, when inner product is introduced, we will show that these are the same. (Contributed by NM, 14-Mar-2014.)
Assertion
Ref Expression
df-doch  |-  ocH  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  ~P ( Base `  ( ( DVecH `  k ) `  w
) )  |->  ( ( ( DIsoH `  k ) `  w ) `  (
( oc `  k
) `  ( ( glb `  k ) `  { y  e.  (
Base `  k )  |  x  C_  ( ( ( DIsoH `  k ) `  w ) `  y
) } ) ) ) ) ) )
Distinct variable group:    w, k, x, y

Detailed syntax breakdown of Definition df-doch
StepHypRef Expression
1 coch 32159 . 2  class  ocH
2 vk . . 3  set  k
3 cvv 2801 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1631 . . . . 5  class  k
6 clh 30795 . . . . 5  class  LHyp
75, 6cfv 5271 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  set  x
94cv 1631 . . . . . . . 8  class  w
10 cdvh 31890 . . . . . . . . 9  class  DVecH
115, 10cfv 5271 . . . . . . . 8  class  ( DVecH `  k )
129, 11cfv 5271 . . . . . . 7  class  ( (
DVecH `  k ) `  w )
13 cbs 13164 . . . . . . 7  class  Base
1412, 13cfv 5271 . . . . . 6  class  ( Base `  ( ( DVecH `  k
) `  w )
)
1514cpw 3638 . . . . 5  class  ~P ( Base `  ( ( DVecH `  k ) `  w
) )
168cv 1631 . . . . . . . . . 10  class  x
17 vy . . . . . . . . . . . 12  set  y
1817cv 1631 . . . . . . . . . . 11  class  y
19 cdih 32040 . . . . . . . . . . . . 13  class  DIsoH
205, 19cfv 5271 . . . . . . . . . . . 12  class  ( DIsoH `  k )
219, 20cfv 5271 . . . . . . . . . . 11  class  ( (
DIsoH `  k ) `  w )
2218, 21cfv 5271 . . . . . . . . . 10  class  ( ( ( DIsoH `  k ) `  w ) `  y
)
2316, 22wss 3165 . . . . . . . . 9  wff  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y )
245, 13cfv 5271 . . . . . . . . 9  class  ( Base `  k )
2523, 17, 24crab 2560 . . . . . . . 8  class  { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) }
26 cglb 14093 . . . . . . . . 9  class  glb
275, 26cfv 5271 . . . . . . . 8  class  ( glb `  k )
2825, 27cfv 5271 . . . . . . 7  class  ( ( glb `  k ) `
 { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) } )
29 coc 13232 . . . . . . . 8  class  oc
305, 29cfv 5271 . . . . . . 7  class  ( oc
`  k )
3128, 30cfv 5271 . . . . . 6  class  ( ( oc `  k ) `
 ( ( glb `  k ) `  {
y  e.  ( Base `  k )  |  x 
C_  ( ( (
DIsoH `  k ) `  w ) `  y
) } ) )
3231, 21cfv 5271 . . . . 5  class  ( ( ( DIsoH `  k ) `  w ) `  (
( oc `  k
) `  ( ( glb `  k ) `  { y  e.  (
Base `  k )  |  x  C_  ( ( ( DIsoH `  k ) `  w ) `  y
) } ) ) )
338, 15, 32cmpt 4093 . . . 4  class  ( x  e.  ~P ( Base `  ( ( DVecH `  k
) `  w )
)  |->  ( ( (
DIsoH `  k ) `  w ) `  (
( oc `  k
) `  ( ( glb `  k ) `  { y  e.  (
Base `  k )  |  x  C_  ( ( ( DIsoH `  k ) `  w ) `  y
) } ) ) ) )
344, 7, 33cmpt 4093 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  ( x  e. 
~P ( Base `  (
( DVecH `  k ) `  w ) )  |->  ( ( ( DIsoH `  k
) `  w ) `  ( ( oc `  k ) `  (
( glb `  k
) `  { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) } ) ) ) ) )
352, 3, 34cmpt 4093 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  ( x  e. 
~P ( Base `  (
( DVecH `  k ) `  w ) )  |->  ( ( ( DIsoH `  k
) `  w ) `  ( ( oc `  k ) `  (
( glb `  k
) `  { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) } ) ) ) ) ) )
361, 35wceq 1632 1  wff  ocH  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  ~P ( Base `  ( ( DVecH `  k ) `  w
) )  |->  ( ( ( DIsoH `  k ) `  w ) `  (
( oc `  k
) `  ( ( glb `  k ) `  { y  e.  (
Base `  k )  |  x  C_  ( ( ( DIsoH `  k ) `  w ) `  y
) } ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  dochffval  32161
  Copyright terms: Public domain W3C validator