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 32083
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 32082 . 2  class  ocH
2 vk . . 3  set  k
3 cvv 2948 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1651 . . . . 5  class  k
6 clh 30718 . . . . 5  class  LHyp
75, 6cfv 5446 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  set  x
94cv 1651 . . . . . . . 8  class  w
10 cdvh 31813 . . . . . . . . 9  class  DVecH
115, 10cfv 5446 . . . . . . . 8  class  ( DVecH `  k )
129, 11cfv 5446 . . . . . . 7  class  ( (
DVecH `  k ) `  w )
13 cbs 13461 . . . . . . 7  class  Base
1412, 13cfv 5446 . . . . . 6  class  ( Base `  ( ( DVecH `  k
) `  w )
)
1514cpw 3791 . . . . 5  class  ~P ( Base `  ( ( DVecH `  k ) `  w
) )
168cv 1651 . . . . . . . . . 10  class  x
17 vy . . . . . . . . . . . 12  set  y
1817cv 1651 . . . . . . . . . . 11  class  y
19 cdih 31963 . . . . . . . . . . . . 13  class  DIsoH
205, 19cfv 5446 . . . . . . . . . . . 12  class  ( DIsoH `  k )
219, 20cfv 5446 . . . . . . . . . . 11  class  ( (
DIsoH `  k ) `  w )
2218, 21cfv 5446 . . . . . . . . . 10  class  ( ( ( DIsoH `  k ) `  w ) `  y
)
2316, 22wss 3312 . . . . . . . . 9  wff  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y )
245, 13cfv 5446 . . . . . . . . 9  class  ( Base `  k )
2523, 17, 24crab 2701 . . . . . . . 8  class  { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) }
26 cglb 14392 . . . . . . . . 9  class  glb
275, 26cfv 5446 . . . . . . . 8  class  ( glb `  k )
2825, 27cfv 5446 . . . . . . 7  class  ( ( glb `  k ) `
 { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) } )
29 coc 13529 . . . . . . . 8  class  oc
305, 29cfv 5446 . . . . . . 7  class  ( oc
`  k )
3128, 30cfv 5446 . . . . . 6  class  ( ( oc `  k ) `
 ( ( glb `  k ) `  {
y  e.  ( Base `  k )  |  x 
C_  ( ( (
DIsoH `  k ) `  w ) `  y
) } ) )
3231, 21cfv 5446 . . . . 5  class  ( ( ( DIsoH `  k ) `  w ) `  (
( oc `  k
) `  ( ( glb `  k ) `  { y  e.  (
Base `  k )  |  x  C_  ( ( ( DIsoH `  k ) `  w ) `  y
) } ) ) )
338, 15, 32cmpt 4258 . . . 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 4258 . . 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 4258 . 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 1652 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  32084
  Copyright terms: Public domain W3C validator