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

Definition df-docaN 31855
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 31854 . 2  class  ocA
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 . . . . . . 7  class  w
10 cltrn 30835 . . . . . . . 8  class  LTrn
115, 10cfv 5446 . . . . . . 7  class  ( LTrn `  k )
129, 11cfv 5446 . . . . . 6  class  ( (
LTrn `  k ) `  w )
1312cpw 3791 . . . . 5  class  ~P (
( LTrn `  k ) `  w )
148cv 1651 . . . . . . . . . . . . 13  class  x
15 vz . . . . . . . . . . . . . 14  set  z
1615cv 1651 . . . . . . . . . . . . 13  class  z
1714, 16wss 3312 . . . . . . . . . . . 12  wff  x  C_  z
18 cdia 31763 . . . . . . . . . . . . . . 15  class  DIsoA
195, 18cfv 5446 . . . . . . . . . . . . . 14  class  ( DIsoA `  k )
209, 19cfv 5446 . . . . . . . . . . . . 13  class  ( (
DIsoA `  k ) `  w )
2120crn 4871 . . . . . . . . . . . 12  class  ran  (
( DIsoA `  k ) `  w )
2217, 15, 21crab 2701 . . . . . . . . . . 11  class  { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z }
2322cint 4042 . . . . . . . . . 10  class  |^| { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z }
2420ccnv 4869 . . . . . . . . . 10  class  `' ( ( DIsoA `  k ) `  w )
2523, 24cfv 5446 . . . . . . . . 9  class  ( `' ( ( DIsoA `  k
) `  w ) `  |^| { z  e. 
ran  ( ( DIsoA `  k ) `  w
)  |  x  C_  z } )
26 coc 13529 . . . . . . . . . 10  class  oc
275, 26cfv 5446 . . . . . . . . 9  class  ( oc
`  k )
2825, 27cfv 5446 . . . . . . . 8  class  ( ( oc `  k ) `
 ( `' ( ( DIsoA `  k ) `  w ) `  |^| { z  e.  ran  (
( DIsoA `  k ) `  w )  |  x 
C_  z } ) )
299, 27cfv 5446 . . . . . . . 8  class  ( ( oc `  k ) `
 w )
30 cjn 14393 . . . . . . . . 9  class  join
315, 30cfv 5446 . . . . . . . 8  class  ( join `  k )
3228, 29, 31co 6073 . . . . . . 7  class  ( ( ( oc `  k
) `  ( `' ( ( DIsoA `  k
) `  w ) `  |^| { z  e. 
ran  ( ( DIsoA `  k ) `  w
)  |  x  C_  z } ) ) (
join `  k )
( ( oc `  k ) `  w
) )
33 cmee 14394 . . . . . . . 8  class  meet
345, 33cfv 5446 . . . . . . 7  class  ( meet `  k )
3532, 9, 34co 6073 . . . . . 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 5446 . . . . 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 4258 . . . 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 4258 . . 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 4258 . 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 1652 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  31856
  Copyright terms: Public domain W3C validator