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 35088
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 35087 . 2  class  ocA
2 vk . . 3  setvar  k
3 cvv 3076 . . 3  class  _V
4 vw . . . 4  setvar  w
52cv 1369 . . . . 5  class  k
6 clh 33951 . . . . 5  class  LHyp
75, 6cfv 5525 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  setvar  x
94cv 1369 . . . . . . 7  class  w
10 cltrn 34068 . . . . . . . 8  class  LTrn
115, 10cfv 5525 . . . . . . 7  class  ( LTrn `  k )
129, 11cfv 5525 . . . . . 6  class  ( (
LTrn `  k ) `  w )
1312cpw 3967 . . . . 5  class  ~P (
( LTrn `  k ) `  w )
148cv 1369 . . . . . . . . . . . . 13  class  x
15 vz . . . . . . . . . . . . . 14  setvar  z
1615cv 1369 . . . . . . . . . . . . 13  class  z
1714, 16wss 3435 . . . . . . . . . . . 12  wff  x  C_  z
18 cdia 34996 . . . . . . . . . . . . . . 15  class  DIsoA
195, 18cfv 5525 . . . . . . . . . . . . . 14  class  ( DIsoA `  k )
209, 19cfv 5525 . . . . . . . . . . . . 13  class  ( (
DIsoA `  k ) `  w )
2120crn 4948 . . . . . . . . . . . 12  class  ran  (
( DIsoA `  k ) `  w )
2217, 15, 21crab 2802 . . . . . . . . . . 11  class  { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z }
2322cint 4235 . . . . . . . . . 10  class  |^| { z  e.  ran  ( (
DIsoA `  k ) `  w )  |  x 
C_  z }
2420ccnv 4946 . . . . . . . . . 10  class  `' ( ( DIsoA `  k ) `  w )
2523, 24cfv 5525 . . . . . . . . 9  class  ( `' ( ( DIsoA `  k
) `  w ) `  |^| { z  e. 
ran  ( ( DIsoA `  k ) `  w
)  |  x  C_  z } )
26 coc 14364 . . . . . . . . . 10  class  oc
275, 26cfv 5525 . . . . . . . . 9  class  ( oc
`  k )
2825, 27cfv 5525 . . . . . . . 8  class  ( ( oc `  k ) `
 ( `' ( ( DIsoA `  k ) `  w ) `  |^| { z  e.  ran  (
( DIsoA `  k ) `  w )  |  x 
C_  z } ) )
299, 27cfv 5525 . . . . . . . 8  class  ( ( oc `  k ) `
 w )
30 cjn 15232 . . . . . . . . 9  class  join
315, 30cfv 5525 . . . . . . . 8  class  ( join `  k )
3228, 29, 31co 6199 . . . . . . 7  class  ( ( ( oc `  k
) `  ( `' ( ( DIsoA `  k
) `  w ) `  |^| { z  e. 
ran  ( ( DIsoA `  k ) `  w
)  |  x  C_  z } ) ) (
join `  k )
( ( oc `  k ) `  w
) )
33 cmee 15233 . . . . . . . 8  class  meet
345, 33cfv 5525 . . . . . . 7  class  ( meet `  k )
3532, 9, 34co 6199 . . . . . 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 5525 . . . . 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 4457 . . . 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 4457 . . 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 4457 . 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 1370 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  35089
  Copyright terms: Public domain W3C validator