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	$$⊢{proj}_1=\left(w\in \mathrm{V}⟼\left(t\in 𝒫{\mathrm{Base}}_w,u\in 𝒫{\mathrm{Base}}_w⟼\left(z\in \left(t\mathrm{LSSum}\left(w\right)u\right)⟼\left(\iota x\in t|\exists y\in uz=x{+}_{w}y\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpj1	$$class{proj}_1$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vt	$$setvart$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarw$$
6	5 4	cfv	$$class{\mathrm{Base}}_w$$
7	6	cpw	$$class𝒫{\mathrm{Base}}_w$$
8		vu	$$setvaru$$
9		vz	$$setvarz$$
10	3	cv	$$setvart$$
11		clsm	$$class\mathrm{LSSum}$$
12	5 11	cfv	$$class\mathrm{LSSum}\left(w\right)$$
13	8	cv	$$setvaru$$
14	10 13 12	co	$$class\left(t\mathrm{LSSum}\left(w\right)u\right)$$
15		vx	$$setvarx$$
16		vy	$$setvary$$
17	9	cv	$$setvarz$$
18	15	cv	$$setvarx$$
19		cplusg	$$class{+}_{𝑔}$$
20	5 19	cfv	$$class{+}_w$$
21	16	cv	$$setvary$$
22	18 21 20	co	$$class\left(x{+}_{w}y\right)$$
23	17 22	wceq	$$wffz=x{+}_{w}y$$
24	23 16 13	wrex	$$wff\exists y\in uz=x{+}_{w}y$$
25	24 15 10	crio	$$class\left(\iota x\in t|\exists y\in uz=x{+}_{w}y\right)$$
26	9 14 25	cmpt	$$class\left(z\in \left(t\mathrm{LSSum}\left(w\right)u\right)⟼\left(\iota x\in t|\exists y\in uz=x{+}_{w}y\right)\right)$$
27	3 8 7 7 26	cmpo	$$class\left(t\in 𝒫{\mathrm{Base}}_w,u\in 𝒫{\mathrm{Base}}_w⟼\left(z\in \left(t\mathrm{LSSum}\left(w\right)u\right)⟼\left(\iota x\in t|\exists y\in uz=x{+}_{w}y\right)\right)\right)$$
28	1 2 27	cmpt	$$class\left(w\in \mathrm{V}⟼\left(t\in 𝒫{\mathrm{Base}}_w,u\in 𝒫{\mathrm{Base}}_w⟼\left(z\in \left(t\mathrm{LSSum}\left(w\right)u\right)⟼\left(\iota x\in t|\exists y\in uz=x{+}_{w}y\right)\right)\right)\right)$$
29	0 28	wceq	$$wff{proj}_1=\left(w\in \mathrm{V}⟼\left(t\in 𝒫{\mathrm{Base}}_w,u\in 𝒫{\mathrm{Base}}_w⟼\left(z\in \left(t\mathrm{LSSum}\left(w\right)u\right)⟼\left(\iota x\in t|\exists y\in uz=x{+}_{w}y\right)\right)\right)\right)$$