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 34625
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 34624 . 2  class  ocH
2 vk . . 3  setvar  k
3 cvv 3087 . . 3  class  _V
4 vw . . . 4  setvar  w
52cv 1436 . . . . 5  class  k
6 clh 33258 . . . . 5  class  LHyp
75, 6cfv 5601 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  setvar  x
94cv 1436 . . . . . . . 8  class  w
10 cdvh 34355 . . . . . . . . 9  class  DVecH
115, 10cfv 5601 . . . . . . . 8  class  ( DVecH `  k )
129, 11cfv 5601 . . . . . . 7  class  ( (
DVecH `  k ) `  w )
13 cbs 15084 . . . . . . 7  class  Base
1412, 13cfv 5601 . . . . . 6  class  ( Base `  ( ( DVecH `  k
) `  w )
)
1514cpw 3985 . . . . 5  class  ~P ( Base `  ( ( DVecH `  k ) `  w
) )
168cv 1436 . . . . . . . . . 10  class  x
17 vy . . . . . . . . . . . 12  setvar  y
1817cv 1436 . . . . . . . . . . 11  class  y
19 cdih 34505 . . . . . . . . . . . . 13  class  DIsoH
205, 19cfv 5601 . . . . . . . . . . . 12  class  ( DIsoH `  k )
219, 20cfv 5601 . . . . . . . . . . 11  class  ( (
DIsoH `  k ) `  w )
2218, 21cfv 5601 . . . . . . . . . 10  class  ( ( ( DIsoH `  k ) `  w ) `  y
)
2316, 22wss 3442 . . . . . . . . 9  wff  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y )
245, 13cfv 5601 . . . . . . . . 9  class  ( Base `  k )
2523, 17, 24crab 2786 . . . . . . . 8  class  { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) }
26 cglb 16139 . . . . . . . . 9  class  glb
275, 26cfv 5601 . . . . . . . 8  class  ( glb `  k )
2825, 27cfv 5601 . . . . . . 7  class  ( ( glb `  k ) `
 { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) } )
29 coc 15160 . . . . . . . 8  class  oc
305, 29cfv 5601 . . . . . . 7  class  ( oc
`  k )
3128, 30cfv 5601 . . . . . 6  class  ( ( oc `  k ) `
 ( ( glb `  k ) `  {
y  e.  ( Base `  k )  |  x 
C_  ( ( (
DIsoH `  k ) `  w ) `  y
) } ) )
3231, 21cfv 5601 . . . . 5  class  ( ( ( DIsoH `  k ) `  w ) `  (
( oc `  k
) `  ( ( glb `  k ) `  { y  e.  (
Base `  k )  |  x  C_  ( ( ( DIsoH `  k ) `  w ) `  y
) } ) ) )
338, 15, 32cmpt 4484 . . . 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 4484 . . 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 4484 . 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 1437 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  34626
  Copyright terms: Public domain W3C validator