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 36145
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 36144 . 2  class  ocH
2 vk . . 3  setvar  k
3 cvv 3113 . . 3  class  _V
4 vw . . . 4  setvar  w
52cv 1378 . . . . 5  class  k
6 clh 34780 . . . . 5  class  LHyp
75, 6cfv 5586 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  setvar  x
94cv 1378 . . . . . . . 8  class  w
10 cdvh 35875 . . . . . . . . 9  class  DVecH
115, 10cfv 5586 . . . . . . . 8  class  ( DVecH `  k )
129, 11cfv 5586 . . . . . . 7  class  ( (
DVecH `  k ) `  w )
13 cbs 14486 . . . . . . 7  class  Base
1412, 13cfv 5586 . . . . . 6  class  ( Base `  ( ( DVecH `  k
) `  w )
)
1514cpw 4010 . . . . 5  class  ~P ( Base `  ( ( DVecH `  k ) `  w
) )
168cv 1378 . . . . . . . . . 10  class  x
17 vy . . . . . . . . . . . 12  setvar  y
1817cv 1378 . . . . . . . . . . 11  class  y
19 cdih 36025 . . . . . . . . . . . . 13  class  DIsoH
205, 19cfv 5586 . . . . . . . . . . . 12  class  ( DIsoH `  k )
219, 20cfv 5586 . . . . . . . . . . 11  class  ( (
DIsoH `  k ) `  w )
2218, 21cfv 5586 . . . . . . . . . 10  class  ( ( ( DIsoH `  k ) `  w ) `  y
)
2316, 22wss 3476 . . . . . . . . 9  wff  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y )
245, 13cfv 5586 . . . . . . . . 9  class  ( Base `  k )
2523, 17, 24crab 2818 . . . . . . . 8  class  { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) }
26 cglb 15426 . . . . . . . . 9  class  glb
275, 26cfv 5586 . . . . . . . 8  class  ( glb `  k )
2825, 27cfv 5586 . . . . . . 7  class  ( ( glb `  k ) `
 { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) } )
29 coc 14559 . . . . . . . 8  class  oc
305, 29cfv 5586 . . . . . . 7  class  ( oc
`  k )
3128, 30cfv 5586 . . . . . 6  class  ( ( oc `  k ) `
 ( ( glb `  k ) `  {
y  e.  ( Base `  k )  |  x 
C_  ( ( (
DIsoH `  k ) `  w ) `  y
) } ) )
3231, 21cfv 5586 . . . . 5  class  ( ( ( DIsoH `  k ) `  w ) `  (
( oc `  k
) `  ( ( glb `  k ) `  { y  e.  (
Base `  k )  |  x  C_  ( ( ( DIsoH `  k ) `  w ) `  y
) } ) ) )
338, 15, 32cmpt 4505 . . . 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 4505 . . 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 4505 . 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 1379 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  36146
  Copyright terms: Public domain W3C validator