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

Definition df-doch 34987
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 34986 . 2  class  ocH
2 vk . . 3  setvar  k
3 cvv 3031 . . 3  class  _V
4 vw . . . 4  setvar  w
52cv 1451 . . . . 5  class  k
6 clh 33620 . . . . 5  class  LHyp
75, 6cfv 5589 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  setvar  x
94cv 1451 . . . . . . . 8  class  w
10 cdvh 34717 . . . . . . . . 9  class  DVecH
115, 10cfv 5589 . . . . . . . 8  class  ( DVecH `  k )
129, 11cfv 5589 . . . . . . 7  class  ( (
DVecH `  k ) `  w )
13 cbs 15199 . . . . . . 7  class  Base
1412, 13cfv 5589 . . . . . 6  class  ( Base `  ( ( DVecH `  k
) `  w )
)
1514cpw 3942 . . . . 5  class  ~P ( Base `  ( ( DVecH `  k ) `  w
) )
168cv 1451 . . . . . . . . . 10  class  x
17 vy . . . . . . . . . . . 12  setvar  y
1817cv 1451 . . . . . . . . . . 11  class  y
19 cdih 34867 . . . . . . . . . . . . 13  class  DIsoH
205, 19cfv 5589 . . . . . . . . . . . 12  class  ( DIsoH `  k )
219, 20cfv 5589 . . . . . . . . . . 11  class  ( (
DIsoH `  k ) `  w )
2218, 21cfv 5589 . . . . . . . . . 10  class  ( ( ( DIsoH `  k ) `  w ) `  y
)
2316, 22wss 3390 . . . . . . . . 9  wff  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y )
245, 13cfv 5589 . . . . . . . . 9  class  ( Base `  k )
2523, 17, 24crab 2760 . . . . . . . 8  class  { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) }
26 cglb 16266 . . . . . . . . 9  class  glb
275, 26cfv 5589 . . . . . . . 8  class  ( glb `  k )
2825, 27cfv 5589 . . . . . . 7  class  ( ( glb `  k ) `
 { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) } )
29 coc 15276 . . . . . . . 8  class  oc
305, 29cfv 5589 . . . . . . 7  class  ( oc
`  k )
3128, 30cfv 5589 . . . . . 6  class  ( ( oc `  k ) `
 ( ( glb `  k ) `  {
y  e.  ( Base `  k )  |  x 
C_  ( ( (
DIsoH `  k ) `  w ) `  y
) } ) )
3231, 21cfv 5589 . . . . 5  class  ( ( ( DIsoH `  k ) `  w ) `  (
( oc `  k
) `  ( ( glb `  k ) `  { y  e.  (
Base `  k )  |  x  C_  ( ( ( DIsoH `  k ) `  w ) `  y
) } ) ) )
338, 15, 32cmpt 4454 . . . 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 4454 . . 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 4454 . 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 1452 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 setvar class
This definition is referenced by:  dochffval  34988
  Copyright terms: Public domain W3C validator