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 = ( 𝑤 ∈ V ↦ ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑤 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ( 𝑧 ∈ ( 𝑡 ( LSSum ‘ 𝑤 ) 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpj1	⊢ proj1
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vt	⊢ 𝑡
4		cbs	⊢ Base
5	1	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( Base ‘ 𝑤 )
7	6	cpw	⊢ 𝒫 ( Base ‘ 𝑤 )
8		vu	⊢ 𝑢
9		vz	⊢ 𝑧
10	3	cv	⊢ 𝑡
11		clsm	⊢ LSSum
12	5 11	cfv	⊢ ( LSSum ‘ 𝑤 )
13	8	cv	⊢ 𝑢
14	10 13 12	co	⊢ ( 𝑡 ( LSSum ‘ 𝑤 ) 𝑢 )
15		vx	⊢ 𝑥
16		vy	⊢ 𝑦
17	9	cv	⊢ 𝑧
18	15	cv	⊢ 𝑥
19		cplusg	⊢ +g
20	5 19	cfv	⊢ ( +g ‘ 𝑤 )
21	16	cv	⊢ 𝑦
22	18 21 20	co	⊢ ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 )
23	17 22	wceq	⊢ 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 )
24	23 16 13	wrex	⊢ ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 )
25	24 15 10	crio	⊢ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) )
26	9 14 25	cmpt	⊢ ( 𝑧 ∈ ( 𝑡 ( LSSum ‘ 𝑤 ) 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) ) )
27	3 8 7 7 26	cmpo	⊢ ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑤 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ( 𝑧 ∈ ( 𝑡 ( LSSum ‘ 𝑤 ) 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) ) ) )
28	1 2 27	cmpt	⊢ ( 𝑤 ∈ V ↦ ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑤 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ( 𝑧 ∈ ( 𝑡 ( LSSum ‘ 𝑤 ) 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) ) ) ) )
29	0 28	wceq	⊢ proj1 = ( 𝑤 ∈ V ↦ ( 𝑡 ∈ 𝒫 ( Base ‘ 𝑤 ) , 𝑢 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ( 𝑧 ∈ ( 𝑡 ( LSSum ‘ 𝑤 ) 𝑢 ) ↦ ( ℩ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝑢 𝑧 = ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) ) ) ) )