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 37260
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 37259 . 2  class  ocA
2 vk . . 3  setvar  k
3 cvv 3034 . . 3  class  _V
4 vw . . . 4  setvar  w
52cv 1398 . . . . 5  class  k
6 clh 36121 . . . . 5  class  LHyp
75, 6cfv 5496 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  setvar  x
94cv 1398 . . . . . . 7  class  w
10 cltrn 36238 . . . . . . . 8  class  LTrn
115, 10cfv 5496 . . . . . . 7  class  ( LTrn `  k )
129, 11cfv 5496 . . . . . 6  class  ( (
LTrn `  k ) `  w )
1312cpw 3927 . . . . 5  class  ~P (
( LTrn `  k ) `  w )
148cv 1398 . . . . . . . . . . . . 13  class  x
15 vz . . . . . . . . . . . . . 14  setvar  z
1615cv 1398 . . . . . . . . . . . . 13  class  z
1714, 16wss 3389 . . . . . . . . . . . 12  wff  x  C_  z
18 cdia 37168 . . . . . . . . . . . . . . 15  class  DIsoA
195, 18cfv 5496 . . . . . . . . . . . . . 14  class  ( DIsoA `  k )
209, 19cfv 5496 . . . . . . . . . . . . 13  class  ( (
DIsoA `  k ) `  w )
2120crn 4914 . . . . . . . . . . . 12  class  ran  (
( DIsoA `  k ) `  w )
2217, 15, 21crab 2736 . . . . . . . . . . 11  class  { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z }
2322cint 4199 . . . . . . . . . 10  class  |^| { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z }
2420ccnv 4912 . . . . . . . . . 10  class  `' ( ( DIsoA `  k ) `  w )
2523, 24cfv 5496 . . . . . . . . 9  class  ( `' ( ( DIsoA `  k
) `  w ) `  |^| { z  e. 
ran  ( ( DIsoA `  k ) `  w
)  |  x  C_  z } )
26 coc 14710 . . . . . . . . . 10  class  oc
275, 26cfv 5496 . . . . . . . . 9  class  ( oc
`  k )
2825, 27cfv 5496 . . . . . . . 8  class  ( ( oc `  k ) `
 ( `' ( ( DIsoA `  k ) `  w ) `  |^| { z  e.  ran  (
( DIsoA `  k ) `  w )  |  x 
C_  z } ) )
299, 27cfv 5496 . . . . . . . 8  class  ( ( oc `  k ) `
 w )
30 cjn 15690 . . . . . . . . 9  class  join
315, 30cfv 5496 . . . . . . . 8  class  ( join `  k )
3228, 29, 31co 6196 . . . . . . 7  class  ( ( ( oc `  k
) `  ( `' ( ( DIsoA `  k
) `  w ) `  |^| { z  e. 
ran  ( ( DIsoA `  k ) `  w
)  |  x  C_  z } ) ) (
join `  k )
( ( oc `  k ) `  w
) )
33 cmee 15691 . . . . . . . 8  class  meet
345, 33cfv 5496 . . . . . . 7  class  ( meet `  k )
3532, 9, 34co 6196 . . . . . 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 5496 . . . . 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 4425 . . . 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 4425 . . 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 4425 . 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 1399 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 setvar class
This definition is referenced by:  docaffvalN  37261
  Copyright terms: Public domain W3C validator