Definition df-pj1 16856

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	|- proj1 = ( 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

Step	Hyp	Ref	Expression
1		cpj1 16854	. 2 class proj1
2		vw	. . 3 setvar w
3		cvv 3106	. . 3 class _V
4		vt	. . . 4 setvar t
5		vu	. . . 4 setvar u
6	2	cv 1397	. . . . . 6 class w
7		cbs 14716	. . . . . 6 class Base
8	6, 7	cfv 5570	. . . . 5 class ( Base ` w )
9	8	cpw 3999	. . . 4 class ~P ( Base ` w )
10		vz	. . . . 5 setvar z
11	4	cv 1397	. . . . . 6 class t
12	5	cv 1397	. . . . . 6 class u
13		clsm 16853	. . . . . . 7 class LSSum
14	6, 13	cfv 5570	. . . . . 6 class ( LSSum ` w )
15	11, 12, 14	co 6270	. . . . 5 class ( t ( LSSum ` w ) u )
16	10	cv 1397	. . . . . . . 8 class z
17		vx	. . . . . . . . . 10 setvar x
18	17	cv 1397	. . . . . . . . 9 class x
19		vy	. . . . . . . . . 10 setvar y
20	19	cv 1397	. . . . . . . . 9 class y
21		cplusg 14784	. . . . . . . . . 10 class +g
22	6, 21	cfv 5570	. . . . . . . . 9 class ( +g ` w )
23	18, 20, 22	co 6270	. . . . . . . 8 class ( x ( +g ` w ) y )
24	16, 23	wceq 1398	. . . . . . 7 wff z = ( x ( +g ` w ) y )
25	24, 19, 12	wrex 2805	. . . . . 6 wff E. y e. u z = ( x ( +g ` w ) y )
26	25, 17, 11	crio 6231	. . . . 5 class ( iota_ x e. t E. y e. u z = ( x ( +g ` w ) y ) )
27	10, 15, 26	cmpt 4497	. . . 4 class ( z e. ( t ( LSSum ` w ) u ) |-> ( iota_ x e. t E. y e. u z = ( x ( +g ` w ) y ) ) )
28	4, 5, 9, 9, 27	cmpt2 6272	. . 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 ) ) ) )
29	2, 3, 28	cmpt 4497	. 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 ) ) ) ) )
30	1, 29	wceq 1398	1 wff proj1 = ( 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 ) ) ) ) )

This definition is referenced by:  pj1fval  16911