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

Definition df-doch 31463
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 31462 . 2  class  ocH
2 vk . . 3  set  k
3 cvv 2899 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1648 . . . . 5  class  k
6 clh 30098 . . . . 5  class  LHyp
75, 6cfv 5394 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  set  x
94cv 1648 . . . . . . . 8  class  w
10 cdvh 31193 . . . . . . . . 9  class  DVecH
115, 10cfv 5394 . . . . . . . 8  class  ( DVecH `  k )
129, 11cfv 5394 . . . . . . 7  class  ( (
DVecH `  k ) `  w )
13 cbs 13396 . . . . . . 7  class  Base
1412, 13cfv 5394 . . . . . 6  class  ( Base `  ( ( DVecH `  k
) `  w )
)
1514cpw 3742 . . . . 5  class  ~P ( Base `  ( ( DVecH `  k ) `  w
) )
168cv 1648 . . . . . . . . . 10  class  x
17 vy . . . . . . . . . . . 12  set  y
1817cv 1648 . . . . . . . . . . 11  class  y
19 cdih 31343 . . . . . . . . . . . . 13  class  DIsoH
205, 19cfv 5394 . . . . . . . . . . . 12  class  ( DIsoH `  k )
219, 20cfv 5394 . . . . . . . . . . 11  class  ( (
DIsoH `  k ) `  w )
2218, 21cfv 5394 . . . . . . . . . 10  class  ( ( ( DIsoH `  k ) `  w ) `  y
)
2316, 22wss 3263 . . . . . . . . 9  wff  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y )
245, 13cfv 5394 . . . . . . . . 9  class  ( Base `  k )
2523, 17, 24crab 2653 . . . . . . . 8  class  { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) }
26 cglb 14327 . . . . . . . . 9  class  glb
275, 26cfv 5394 . . . . . . . 8  class  ( glb `  k )
2825, 27cfv 5394 . . . . . . 7  class  ( ( glb `  k ) `
 { y  e.  ( Base `  k
)  |  x  C_  ( ( ( DIsoH `  k ) `  w
) `  y ) } )
29 coc 13464 . . . . . . . 8  class  oc
305, 29cfv 5394 . . . . . . 7  class  ( oc
`  k )
3128, 30cfv 5394 . . . . . 6  class  ( ( oc `  k ) `
 ( ( glb `  k ) `  {
y  e.  ( Base `  k )  |  x 
C_  ( ( (
DIsoH `  k ) `  w ) `  y
) } ) )
3231, 21cfv 5394 . . . . 5  class  ( ( ( DIsoH `  k ) `  w ) `  (
( oc `  k
) `  ( ( glb `  k ) `  { y  e.  (
Base `  k )  |  x  C_  ( ( ( DIsoH `  k ) `  w ) `  y
) } ) ) )
338, 15, 32cmpt 4207 . . . 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 4207 . . 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 4207 . 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 1649 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  31464
  Copyright terms: Public domain W3C validator