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

Definition df-docaN 31235
Description: Define subspace orthocomplement for  DVecA partial 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, 6-Dec-2013.)
Assertion
Ref Expression
df-docaN  |-  ocA  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  ~P (
( LTrn `  k ) `  w )  |->  ( ( ( DIsoA `  k ) `  w ) `  (
( ( ( oc
`  k ) `  ( `' ( ( DIsoA `  k ) `  w
) `  |^| { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z } ) ) ( join `  k
) ( ( oc
`  k ) `  w ) ) (
meet `  k )
w ) ) ) ) )
Distinct variable group:    w, k, x, z

Detailed syntax breakdown of Definition df-docaN
StepHypRef Expression
1 cocaN 31234 . 2  class  ocA
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 . . . . . . 7  class  w
10 cltrn 30215 . . . . . . . 8  class  LTrn
115, 10cfv 5394 . . . . . . 7  class  ( LTrn `  k )
129, 11cfv 5394 . . . . . 6  class  ( (
LTrn `  k ) `  w )
1312cpw 3742 . . . . 5  class  ~P (
( LTrn `  k ) `  w )
148cv 1648 . . . . . . . . . . . . 13  class  x
15 vz . . . . . . . . . . . . . 14  set  z
1615cv 1648 . . . . . . . . . . . . 13  class  z
1714, 16wss 3263 . . . . . . . . . . . 12  wff  x  C_  z
18 cdia 31143 . . . . . . . . . . . . . . 15  class  DIsoA
195, 18cfv 5394 . . . . . . . . . . . . . 14  class  ( DIsoA `  k )
209, 19cfv 5394 . . . . . . . . . . . . 13  class  ( (
DIsoA `  k ) `  w )
2120crn 4819 . . . . . . . . . . . 12  class  ran  (
( DIsoA `  k ) `  w )
2217, 15, 21crab 2653 . . . . . . . . . . 11  class  { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z }
2322cint 3992 . . . . . . . . . 10  class  |^| { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z }
2420ccnv 4817 . . . . . . . . . 10  class  `' ( ( DIsoA `  k ) `  w )
2523, 24cfv 5394 . . . . . . . . 9  class  ( `' ( ( DIsoA `  k
) `  w ) `  |^| { z  e. 
ran  ( ( DIsoA `  k ) `  w
)  |  x  C_  z } )
26 coc 13464 . . . . . . . . . 10  class  oc
275, 26cfv 5394 . . . . . . . . 9  class  ( oc
`  k )
2825, 27cfv 5394 . . . . . . . 8  class  ( ( oc `  k ) `
 ( `' ( ( DIsoA `  k ) `  w ) `  |^| { z  e.  ran  (
( DIsoA `  k ) `  w )  |  x 
C_  z } ) )
299, 27cfv 5394 . . . . . . . 8  class  ( ( oc `  k ) `
 w )
30 cjn 14328 . . . . . . . . 9  class  join
315, 30cfv 5394 . . . . . . . 8  class  ( join `  k )
3228, 29, 31co 6020 . . . . . . 7  class  ( ( ( oc `  k
) `  ( `' ( ( DIsoA `  k
) `  w ) `  |^| { z  e. 
ran  ( ( DIsoA `  k ) `  w
)  |  x  C_  z } ) ) (
join `  k )
( ( oc `  k ) `  w
) )
33 cmee 14329 . . . . . . . 8  class  meet
345, 33cfv 5394 . . . . . . 7  class  ( meet `  k )
3532, 9, 34co 6020 . . . . . 6  class  ( ( ( ( oc `  k ) `  ( `' ( ( DIsoA `  k ) `  w
) `  |^| { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z } ) ) ( join `  k
) ( ( oc
`  k ) `  w ) ) (
meet `  k )
w )
3635, 20cfv 5394 . . . . 5  class  ( ( ( DIsoA `  k ) `  w ) `  (
( ( ( oc
`  k ) `  ( `' ( ( DIsoA `  k ) `  w
) `  |^| { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z } ) ) ( join `  k
) ( ( oc
`  k ) `  w ) ) (
meet `  k )
w ) )
378, 13, 36cmpt 4207 . . . 4  class  ( x  e.  ~P ( (
LTrn `  k ) `  w )  |->  ( ( ( DIsoA `  k ) `  w ) `  (
( ( ( oc
`  k ) `  ( `' ( ( DIsoA `  k ) `  w
) `  |^| { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z } ) ) ( join `  k
) ( ( oc
`  k ) `  w ) ) (
meet `  k )
w ) ) )
384, 7, 37cmpt 4207 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  ( x  e. 
~P ( ( LTrn `  k ) `  w
)  |->  ( ( (
DIsoA `  k ) `  w ) `  (
( ( ( oc
`  k ) `  ( `' ( ( DIsoA `  k ) `  w
) `  |^| { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z } ) ) ( join `  k
) ( ( oc
`  k ) `  w ) ) (
meet `  k )
w ) ) ) )
392, 3, 38cmpt 4207 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  ( x  e. 
~P ( ( LTrn `  k ) `  w
)  |->  ( ( (
DIsoA `  k ) `  w ) `  (
( ( ( oc
`  k ) `  ( `' ( ( DIsoA `  k ) `  w
) `  |^| { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z } ) ) ( join `  k
) ( ( oc
`  k ) `  w ) ) (
meet `  k )
w ) ) ) ) )
401, 39wceq 1649 1  wff  ocA  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  ~P (
( LTrn `  k ) `  w )  |->  ( ( ( DIsoA `  k ) `  w ) `  (
( ( ( oc
`  k ) `  ( `' ( ( DIsoA `  k ) `  w
) `  |^| { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z } ) ) ( join `  k
) ( ( oc
`  k ) `  w ) ) (
meet `  k )
w ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  docaffvalN  31236
  Copyright terms: Public domain W3C validator