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

Definition df-doch 34998
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 34997 . 2  class  ocH
2 vk . . 3  setvar  k
3 cvv 2977 . . 3  class  _V
4 vw . . . 4  setvar  w
52cv 1368 . . . . 5  class  k
6 clh 33633 . . . . 5  class  LHyp
75, 6cfv 5423 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  setvar  x
94cv 1368 . . . . . . . 8  class  w
10 cdvh 34728 . . . . . . . . 9  class  DVecH
115, 10cfv 5423 . . . . . . . 8  class  ( DVecH `  k )
129, 11cfv 5423 . . . . . . 7  class  ( (
DVecH `  k ) `  w )
13 cbs 14179 . . . . . . 7  class  Base
1412, 13cfv 5423 . . . . . 6  class  ( Base `  ( ( DVecH `  k
) `  w )
)
1514cpw 3865 . . . . 5  class  ~P ( Base `  ( ( DVecH `  k ) `  w
) )
168cv 1368 . . . . . . . . . 10  class  x
17 vy . . . . . . . . . . . 12  setvar  y
1817cv 1368 . . . . . . . . . . 11  class  y
19 cdih 34878 . . . . . . . . . . . . 13  class  DIsoH
205, 19cfv 5423 . . . . . . . . . . . 12  class  ( DIsoH `  k )
219, 20cfv 5423 . . . . . . . . . . 11  class  ( (
DIsoH `  k ) `  w )
2218, 21cfv 5423 . . . . . . . . . 10  class  ( ( ( DIsoH `  k ) `  w ) `  y
)
2316, 22wss 3333 . . . . . . . . 9  wff  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y )
245, 13cfv 5423 . . . . . . . . 9  class  ( Base `  k )
2523, 17, 24crab 2724 . . . . . . . 8  class  { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) }
26 cglb 15118 . . . . . . . . 9  class  glb
275, 26cfv 5423 . . . . . . . 8  class  ( glb `  k )
2825, 27cfv 5423 . . . . . . 7  class  ( ( glb `  k ) `
 { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) } )
29 coc 14251 . . . . . . . 8  class  oc
305, 29cfv 5423 . . . . . . 7  class  ( oc
`  k )
3128, 30cfv 5423 . . . . . 6  class  ( ( oc `  k ) `
 ( ( glb `  k ) `  {
y  e.  ( Base `  k )  |  x 
C_  ( ( (
DIsoH `  k ) `  w ) `  y
) } ) )
3231, 21cfv 5423 . . . . 5  class  ( ( ( DIsoH `  k ) `  w ) `  (
( oc `  k
) `  ( ( glb `  k ) `  { y  e.  (
Base `  k )  |  x  C_  ( ( ( DIsoH `  k ) `  w ) `  y
) } ) ) )
338, 15, 32cmpt 4355 . . . 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 4355 . . 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 4355 . 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 1369 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  34999
  Copyright terms: Public domain W3C validator