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

Definition df-docaN 31310
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 31309 . 2  class  ocA
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 . . . . . . 7  class  w
10 cltrn 30290 . . . . . . . 8  class  LTrn
115, 10cfv 5255 . . . . . . 7  class  ( LTrn `  k )
129, 11cfv 5255 . . . . . 6  class  ( (
LTrn `  k ) `  w )
1312cpw 3625 . . . . 5  class  ~P (
( LTrn `  k ) `  w )
148cv 1622 . . . . . . . . . . . . 13  class  x
15 vz . . . . . . . . . . . . . 14  set  z
1615cv 1622 . . . . . . . . . . . . 13  class  z
1714, 16wss 3152 . . . . . . . . . . . 12  wff  x  C_  z
18 cdia 31218 . . . . . . . . . . . . . . 15  class  DIsoA
195, 18cfv 5255 . . . . . . . . . . . . . 14  class  ( DIsoA `  k )
209, 19cfv 5255 . . . . . . . . . . . . 13  class  ( (
DIsoA `  k ) `  w )
2120crn 4690 . . . . . . . . . . . 12  class  ran  (
( DIsoA `  k ) `  w )
2217, 15, 21crab 2547 . . . . . . . . . . 11  class  { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z }
2322cint 3862 . . . . . . . . . 10  class  |^| { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z }
2420ccnv 4688 . . . . . . . . . 10  class  `' ( ( DIsoA `  k ) `  w )
2523, 24cfv 5255 . . . . . . . . 9  class  ( `' ( ( DIsoA `  k
) `  w ) `  |^| { z  e. 
ran  ( ( DIsoA `  k ) `  w
)  |  x  C_  z } )
26 coc 13216 . . . . . . . . . 10  class  oc
275, 26cfv 5255 . . . . . . . . 9  class  ( oc
`  k )
2825, 27cfv 5255 . . . . . . . 8  class  ( ( oc `  k ) `
 ( `' ( ( DIsoA `  k ) `  w ) `  |^| { z  e.  ran  (
( DIsoA `  k ) `  w )  |  x 
C_  z } ) )
299, 27cfv 5255 . . . . . . . 8  class  ( ( oc `  k ) `
 w )
30 cjn 14078 . . . . . . . . 9  class  join
315, 30cfv 5255 . . . . . . . 8  class  ( join `  k )
3228, 29, 31co 5858 . . . . . . 7  class  ( ( ( oc `  k
) `  ( `' ( ( DIsoA `  k
) `  w ) `  |^| { z  e. 
ran  ( ( DIsoA `  k ) `  w
)  |  x  C_  z } ) ) (
join `  k )
( ( oc `  k ) `  w
) )
33 cmee 14079 . . . . . . . 8  class  meet
345, 33cfv 5255 . . . . . . 7  class  ( meet `  k )
3532, 9, 34co 5858 . . . . . 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 5255 . . . . 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 4077 . . . 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 4077 . . 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 4077 . 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 1623 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  31311
  Copyright terms: Public domain W3C validator