Definition df-pj1 17875

Description: Define the left projection function, which takes two subgroups 𝑡, 𝑢 with trivial intersection and returns a function mapping the elements of the subgroup sum 𝑡 + 𝑢 to their projections onto 𝑡. (The other projection function can be obtained by swapping the roles of 𝑡 and 𝑢.) (Contributed by Mario Carneiro, 15-Oct-2015.)

Assertion

Ref	Expression
df-pj1	⊢ proj1 = (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ (𝑧 ∈ (𝑡(LSSum‘𝑤)𝑢) ↦ (℩𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝑢 𝑧 = (𝑥(+g‘𝑤)𝑦)))))

Distinct variable group:   𝑤,𝑡,𝑢,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-pj1

Step	Hyp	Ref	Expression
1		cpj1 17873	. 2 class proj1
2		vw	. . 3 setvar 𝑤
3		cvv 3173	. . 3 class V
4		vt	. . . 4 setvar 𝑡
5		vu	. . . 4 setvar 𝑢
6	2	cv 1474	. . . . . 6 class 𝑤
7		cbs 15695	. . . . . 6 class Base
8	6, 7	cfv 5804	. . . . 5 class (Base‘𝑤)
9	8	cpw 4108	. . . 4 class 𝒫 (Base‘𝑤)
10		vz	. . . . 5 setvar 𝑧
11	4	cv 1474	. . . . . 6 class 𝑡
12	5	cv 1474	. . . . . 6 class 𝑢
13		clsm 17872	. . . . . . 7 class LSSum
14	6, 13	cfv 5804	. . . . . 6 class (LSSum‘𝑤)
15	11, 12, 14	co 6549	. . . . 5 class (𝑡(LSSum‘𝑤)𝑢)
16	10	cv 1474	. . . . . . . 8 class 𝑧
17		vx	. . . . . . . . . 10 setvar 𝑥
18	17	cv 1474	. . . . . . . . 9 class 𝑥
19		vy	. . . . . . . . . 10 setvar 𝑦
20	19	cv 1474	. . . . . . . . 9 class 𝑦
21		cplusg 15768	. . . . . . . . . 10 class +g
22	6, 21	cfv 5804	. . . . . . . . 9 class (+g‘𝑤)
23	18, 20, 22	co 6549	. . . . . . . 8 class (𝑥(+g‘𝑤)𝑦)
24	16, 23	wceq 1475	. . . . . . 7 wff 𝑧 = (𝑥(+g‘𝑤)𝑦)
25	24, 19, 12	wrex 2897	. . . . . 6 wff ∃𝑦 ∈ 𝑢 𝑧 = (𝑥(+g‘𝑤)𝑦)
26	25, 17, 11	crio 6510	. . . . 5 class (℩𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝑢 𝑧 = (𝑥(+g‘𝑤)𝑦))
27	10, 15, 26	cmpt 4643	. . . 4 class (𝑧 ∈ (𝑡(LSSum‘𝑤)𝑢) ↦ (℩𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝑢 𝑧 = (𝑥(+g‘𝑤)𝑦)))
28	4, 5, 9, 9, 27	cmpt2 6551	. . 3 class (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ (𝑧 ∈ (𝑡(LSSum‘𝑤)𝑢) ↦ (℩𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝑢 𝑧 = (𝑥(+g‘𝑤)𝑦))))
29	2, 3, 28	cmpt 4643	. 2 class (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ (𝑧 ∈ (𝑡(LSSum‘𝑤)𝑢) ↦ (℩𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝑢 𝑧 = (𝑥(+g‘𝑤)𝑦)))))
30	1, 29	wceq 1475	1 wff proj1 = (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ (𝑧 ∈ (𝑡(LSSum‘𝑤)𝑢) ↦ (℩𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝑢 𝑧 = (𝑥(+g‘𝑤)𝑦)))))

This definition is referenced by:  pj1fval  17930