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

Definition df-djaN 31944
Description: Define (closed) subspace join for  DVecA partial vector space. (Contributed by NM, 6-Dec-2013.)
Assertion
Ref Expression
df-djaN  |-  vA  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  ~P (
( LTrn `  k ) `  w ) ,  y  e.  ~P ( (
LTrn `  k ) `  w )  |->  ( ( ( ocA `  k
) `  w ) `  ( ( ( ( ocA `  k ) `
 w ) `  x )  i^i  (
( ( ocA `  k
) `  w ) `  y ) ) ) ) ) )
Distinct variable group:    w, k, x, y

Detailed syntax breakdown of Definition df-djaN
StepHypRef Expression
1 cdjaN 31943 . 2  class  vA
2 vk . . 3  set  k
3 cvv 2801 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1631 . . . . 5  class  k
6 clh 30795 . . . . 5  class  LHyp
75, 6cfv 5271 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  set  x
9 vy . . . . 5  set  y
104cv 1631 . . . . . . 7  class  w
11 cltrn 30912 . . . . . . . 8  class  LTrn
125, 11cfv 5271 . . . . . . 7  class  ( LTrn `  k )
1310, 12cfv 5271 . . . . . 6  class  ( (
LTrn `  k ) `  w )
1413cpw 3638 . . . . 5  class  ~P (
( LTrn `  k ) `  w )
158cv 1631 . . . . . . . 8  class  x
16 cocaN 31931 . . . . . . . . . 10  class  ocA
175, 16cfv 5271 . . . . . . . . 9  class  ( ocA `  k )
1810, 17cfv 5271 . . . . . . . 8  class  ( ( ocA `  k ) `
 w )
1915, 18cfv 5271 . . . . . . 7  class  ( ( ( ocA `  k
) `  w ) `  x )
209cv 1631 . . . . . . . 8  class  y
2120, 18cfv 5271 . . . . . . 7  class  ( ( ( ocA `  k
) `  w ) `  y )
2219, 21cin 3164 . . . . . 6  class  ( ( ( ( ocA `  k
) `  w ) `  x )  i^i  (
( ( ocA `  k
) `  w ) `  y ) )
2322, 18cfv 5271 . . . . 5  class  ( ( ( ocA `  k
) `  w ) `  ( ( ( ( ocA `  k ) `
 w ) `  x )  i^i  (
( ( ocA `  k
) `  w ) `  y ) ) )
248, 9, 14, 14, 23cmpt2 5876 . . . 4  class  ( x  e.  ~P ( (
LTrn `  k ) `  w ) ,  y  e.  ~P ( (
LTrn `  k ) `  w )  |->  ( ( ( ocA `  k
) `  w ) `  ( ( ( ( ocA `  k ) `
 w ) `  x )  i^i  (
( ( ocA `  k
) `  w ) `  y ) ) ) )
254, 7, 24cmpt 4093 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  ( x  e. 
~P ( ( LTrn `  k ) `  w
) ,  y  e. 
~P ( ( LTrn `  k ) `  w
)  |->  ( ( ( ocA `  k ) `
 w ) `  ( ( ( ( ocA `  k ) `
 w ) `  x )  i^i  (
( ( ocA `  k
) `  w ) `  y ) ) ) ) )
262, 3, 25cmpt 4093 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  ( x  e. 
~P ( ( LTrn `  k ) `  w
) ,  y  e. 
~P ( ( LTrn `  k ) `  w
)  |->  ( ( ( ocA `  k ) `
 w ) `  ( ( ( ( ocA `  k ) `
 w ) `  x )  i^i  (
( ( ocA `  k
) `  w ) `  y ) ) ) ) ) )
271, 26wceq 1632 1  wff  vA  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  ~P (
( LTrn `  k ) `  w ) ,  y  e.  ~P ( (
LTrn `  k ) `  w )  |->  ( ( ( ocA `  k
) `  w ) `  ( ( ( ( ocA `  k ) `
 w ) `  x )  i^i  (
( ( ocA `  k
) `  w ) `  y ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  djaffvalN  31945
  Copyright terms: Public domain W3C validator