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

Definition df-doch 31611
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 31610 . 2  class  ocH
2 vk . . 3  set  k
3 cvv 2790 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1624 . . . . 5  class  k
6 clh 30246 . . . . 5  class  LHyp
75, 6cfv 5257 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  set  x
94cv 1624 . . . . . . . 8  class  w
10 cdvh 31341 . . . . . . . . 9  class  DVecH
115, 10cfv 5257 . . . . . . . 8  class  ( DVecH `  k )
129, 11cfv 5257 . . . . . . 7  class  ( (
DVecH `  k ) `  w )
13 cbs 13150 . . . . . . 7  class  Base
1412, 13cfv 5257 . . . . . 6  class  ( Base `  ( ( DVecH `  k
) `  w )
)
1514cpw 3627 . . . . 5  class  ~P ( Base `  ( ( DVecH `  k ) `  w
) )
168cv 1624 . . . . . . . . . 10  class  x
17 vy . . . . . . . . . . . 12  set  y
1817cv 1624 . . . . . . . . . . 11  class  y
19 cdih 31491 . . . . . . . . . . . . 13  class  DIsoH
205, 19cfv 5257 . . . . . . . . . . . 12  class  ( DIsoH `  k )
219, 20cfv 5257 . . . . . . . . . . 11  class  ( (
DIsoH `  k ) `  w )
2218, 21cfv 5257 . . . . . . . . . 10  class  ( ( ( DIsoH `  k ) `  w ) `  y
)
2316, 22wss 3154 . . . . . . . . 9  wff  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y )
245, 13cfv 5257 . . . . . . . . 9  class  ( Base `  k )
2523, 17, 24crab 2549 . . . . . . . 8  class  { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) }
26 cglb 14079 . . . . . . . . 9  class  glb
275, 26cfv 5257 . . . . . . . 8  class  ( glb `  k )
2825, 27cfv 5257 . . . . . . 7  class  ( ( glb `  k ) `
 { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) } )
29 coc 13218 . . . . . . . 8  class  oc
305, 29cfv 5257 . . . . . . 7  class  ( oc
`  k )
3128, 30cfv 5257 . . . . . 6  class  ( ( oc `  k ) `
 ( ( glb `  k ) `  {
y  e.  ( Base `  k )  |  x 
C_  ( ( (
DIsoH `  k ) `  w ) `  y
) } ) )
3231, 21cfv 5257 . . . . 5  class  ( ( ( DIsoH `  k ) `  w ) `  (
( oc `  k
) `  ( ( glb `  k ) `  { y  e.  (
Base `  k )  |  x  C_  ( ( ( DIsoH `  k ) `  w ) `  y
) } ) ) )
338, 15, 32cmpt 4079 . . . 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 4079 . . 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 4079 . 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 1625 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  31612
  Copyright terms: Public domain W3C validator