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 37491
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 37490 . 2  class  ocH
2 vk . . 3  setvar  k
3 cvv 3106 . . 3  class  _V
4 vw . . . 4  setvar  w
52cv 1397 . . . . 5  class  k
6 clh 36124 . . . . 5  class  LHyp
75, 6cfv 5570 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  setvar  x
94cv 1397 . . . . . . . 8  class  w
10 cdvh 37221 . . . . . . . . 9  class  DVecH
115, 10cfv 5570 . . . . . . . 8  class  ( DVecH `  k )
129, 11cfv 5570 . . . . . . 7  class  ( (
DVecH `  k ) `  w )
13 cbs 14719 . . . . . . 7  class  Base
1412, 13cfv 5570 . . . . . 6  class  ( Base `  ( ( DVecH `  k
) `  w )
)
1514cpw 3999 . . . . 5  class  ~P ( Base `  ( ( DVecH `  k ) `  w
) )
168cv 1397 . . . . . . . . . 10  class  x
17 vy . . . . . . . . . . . 12  setvar  y
1817cv 1397 . . . . . . . . . . 11  class  y
19 cdih 37371 . . . . . . . . . . . . 13  class  DIsoH
205, 19cfv 5570 . . . . . . . . . . . 12  class  ( DIsoH `  k )
219, 20cfv 5570 . . . . . . . . . . 11  class  ( (
DIsoH `  k ) `  w )
2218, 21cfv 5570 . . . . . . . . . 10  class  ( ( ( DIsoH `  k ) `  w ) `  y
)
2316, 22wss 3461 . . . . . . . . 9  wff  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y )
245, 13cfv 5570 . . . . . . . . 9  class  ( Base `  k )
2523, 17, 24crab 2808 . . . . . . . 8  class  { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) }
26 cglb 15774 . . . . . . . . 9  class  glb
275, 26cfv 5570 . . . . . . . 8  class  ( glb `  k )
2825, 27cfv 5570 . . . . . . 7  class  ( ( glb `  k ) `
 { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) } )
29 coc 14795 . . . . . . . 8  class  oc
305, 29cfv 5570 . . . . . . 7  class  ( oc
`  k )
3128, 30cfv 5570 . . . . . 6  class  ( ( oc `  k ) `
 ( ( glb `  k ) `  {
y  e.  ( Base `  k )  |  x 
C_  ( ( (
DIsoH `  k ) `  w ) `  y
) } ) )
3231, 21cfv 5570 . . . . 5  class  ( ( ( DIsoH `  k ) `  w ) `  (
( oc `  k
) `  ( ( glb `  k ) `  { y  e.  (
Base `  k )  |  x  C_  ( ( ( DIsoH `  k ) `  w ) `  y
) } ) ) )
338, 15, 32cmpt 4497 . . . 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 4497 . . 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 4497 . 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 1398 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  37492
  Copyright terms: Public domain W3C validator