Definition df-pj1

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)

	Ref	Expression
Assertion	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 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpj1	|- proj1
1		vw	|- w
2		cvv	|- _V
3		vt	|- t
4		cbs	|- Base
5	1	cv	|- w
6	5 4	cfv	|- ( Base ` w )
7	6	cpw	|- ~P ( Base ` w )
8		vu	|- u
9		vz	|- z
10	3	cv	|- t
11		clsm	|- LSSum
12	5 11	cfv	|- ( LSSum ` w )
13	8	cv	|- u
14	10 13 12	co	|- ( t ( LSSum ` w ) u )
15		vx	|- x
16		vy	|- y
17	9	cv	|- z
18	15	cv	|- x
19		cplusg	|- +g
20	5 19	cfv	|- ( +g ` w )
21	16	cv	|- y
22	18 21 20	co	|- ( x ( +g ` w ) y )
23	17 22	wceq	|- z = ( x ( +g ` w ) y )
24	23 16 13	wrex	|- E. y e. u z = ( x ( +g ` w ) y )
25	24 15 10	crio	|- ( iota_ x e. t E. y e. u z = ( x ( +g ` w ) y ) )
26	9 14 25	cmpt	|- ( z e. ( t ( LSSum ` w ) u ) |-> ( iota_ x e. t E. y e. u z = ( x ( +g ` w ) y ) ) )
27	3 8 7 7 26	cmpo	|- ( 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 ) ) ) )
28	1 2 27	cmpt	|- ( 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 ) ) ) ) )
29	0 28	wceq	|- 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 ) ) ) ) )