MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pj1 Unicode version

Definition df-pj1 14964
Description: Define the left projection function, which takes two subgroups  t ,  u with trivial intersection and returns a function mapping the elements of the subgroup sum  t  +  u to their projections onto  t. (The other projection function can be obtained by swapping the roles of  t and  u.) (Contributed by Mario Carneiro, 15-Oct-2015.)
Assertion
Ref Expression
df-pj1  |-  proj 1  =  ( w  e. 
_V  |->  ( t  e. 
~P ( Base `  w
) ,  u  e. 
~P ( Base `  w
)  |->  ( z  e.  ( t ( LSSum `  w ) u ) 
|->  ( iota_ x  e.  t E. y  e.  u  z  =  ( x
( +g  `  w ) y ) ) ) ) )
Distinct variable group:    w, t, u, x, y, z

Detailed syntax breakdown of Definition df-pj1
StepHypRef Expression
1 cpj1 14962 . 2  class  proj 1
2 vw . . 3  set  w
3 cvv 2801 . . 3  class  _V
4 vt . . . 4  set  t
5 vu . . . 4  set  u
62cv 1631 . . . . . 6  class  w
7 cbs 13164 . . . . . 6  class  Base
86, 7cfv 5271 . . . . 5  class  ( Base `  w )
98cpw 3638 . . . 4  class  ~P ( Base `  w )
10 vz . . . . 5  set  z
114cv 1631 . . . . . 6  class  t
125cv 1631 . . . . . 6  class  u
13 clsm 14961 . . . . . . 7  class  LSSum
146, 13cfv 5271 . . . . . 6  class  ( LSSum `  w )
1511, 12, 14co 5874 . . . . 5  class  ( t ( LSSum `  w )
u )
1610cv 1631 . . . . . . . 8  class  z
17 vx . . . . . . . . . 10  set  x
1817cv 1631 . . . . . . . . 9  class  x
19 vy . . . . . . . . . 10  set  y
2019cv 1631 . . . . . . . . 9  class  y
21 cplusg 13224 . . . . . . . . . 10  class  +g
226, 21cfv 5271 . . . . . . . . 9  class  ( +g  `  w )
2318, 20, 22co 5874 . . . . . . . 8  class  ( x ( +g  `  w
) y )
2416, 23wceq 1632 . . . . . . 7  wff  z  =  ( x ( +g  `  w ) y )
2524, 19, 12wrex 2557 . . . . . 6  wff  E. y  e.  u  z  =  ( x ( +g  `  w ) y )
2625, 17, 11crio 6313 . . . . 5  class  ( iota_ x  e.  t E. y  e.  u  z  =  ( x ( +g  `  w ) y ) )
2710, 15, 26cmpt 4093 . . . 4  class  ( z  e.  ( t (
LSSum `  w ) u )  |->  ( iota_ x  e.  t E. y  e.  u  z  =  ( x ( +g  `  w
) y ) ) )
284, 5, 9, 9, 27cmpt2 5876 . . 3  class  ( t  e.  ~P ( Base `  w ) ,  u  e.  ~P ( Base `  w
)  |->  ( z  e.  ( t ( LSSum `  w ) u ) 
|->  ( iota_ x  e.  t E. y  e.  u  z  =  ( x
( +g  `  w ) y ) ) ) )
292, 3, 28cmpt 4093 . 2  class  ( w  e.  _V  |->  ( t  e.  ~P ( Base `  w ) ,  u  e.  ~P ( Base `  w
)  |->  ( z  e.  ( t ( LSSum `  w ) u ) 
|->  ( iota_ x  e.  t E. y  e.  u  z  =  ( x
( +g  `  w ) y ) ) ) ) )
301, 29wceq 1632 1  wff  proj 1  =  ( w  e. 
_V  |->  ( t  e. 
~P ( Base `  w
) ,  u  e. 
~P ( Base `  w
)  |->  ( z  e.  ( t ( LSSum `  w ) u ) 
|->  ( iota_ x  e.  t E. y  e.  u  z  =  ( x
( +g  `  w ) y ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  pj1fval  15019
  Copyright terms: Public domain W3C validator