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

Definition df-doch 31538
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 31537 . 2  class  ocH
2 vk . . 3  set  k
3 cvv 2788 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1622 . . . . 5  class  k
6 clh 30173 . . . . 5  class  LHyp
75, 6cfv 5255 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  set  x
94cv 1622 . . . . . . . 8  class  w
10 cdvh 31268 . . . . . . . . 9  class  DVecH
115, 10cfv 5255 . . . . . . . 8  class  ( DVecH `  k )
129, 11cfv 5255 . . . . . . 7  class  ( (
DVecH `  k ) `  w )
13 cbs 13148 . . . . . . 7  class  Base
1412, 13cfv 5255 . . . . . 6  class  ( Base `  ( ( DVecH `  k
) `  w )
)
1514cpw 3625 . . . . 5  class  ~P ( Base `  ( ( DVecH `  k ) `  w
) )
168cv 1622 . . . . . . . . . 10  class  x
17 vy . . . . . . . . . . . 12  set  y
1817cv 1622 . . . . . . . . . . 11  class  y
19 cdih 31418 . . . . . . . . . . . . 13  class  DIsoH
205, 19cfv 5255 . . . . . . . . . . . 12  class  ( DIsoH `  k )
219, 20cfv 5255 . . . . . . . . . . 11  class  ( (
DIsoH `  k ) `  w )
2218, 21cfv 5255 . . . . . . . . . 10  class  ( ( ( DIsoH `  k ) `  w ) `  y
)
2316, 22wss 3152 . . . . . . . . 9  wff  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y )
245, 13cfv 5255 . . . . . . . . 9  class  ( Base `  k )
2523, 17, 24crab 2547 . . . . . . . 8  class  { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) }
26 cglb 14077 . . . . . . . . 9  class  glb
275, 26cfv 5255 . . . . . . . 8  class  ( glb `  k )
2825, 27cfv 5255 . . . . . . 7  class  ( ( glb `  k ) `
 { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) } )
29 coc 13216 . . . . . . . 8  class  oc
305, 29cfv 5255 . . . . . . 7  class  ( oc
`  k )
3128, 30cfv 5255 . . . . . 6  class  ( ( oc `  k ) `
 ( ( glb `  k ) `  {
y  e.  ( Base `  k )  |  x 
C_  ( ( (
DIsoH `  k ) `  w ) `  y
) } ) )
3231, 21cfv 5255 . . . . 5  class  ( ( ( DIsoH `  k ) `  w ) `  (
( oc `  k
) `  ( ( glb `  k ) `  { y  e.  (
Base `  k )  |  x  C_  ( ( ( DIsoH `  k ) `  w ) `  y
) } ) ) )
338, 15, 32cmpt 4077 . . . 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 4077 . . 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 4077 . 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 1623 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 set class
This definition is referenced by:  dochffval  31539
  Copyright terms: Public domain W3C validator