Metamath Proof Explorer

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 = w ∈ V ⟼ t ∈ 𝒫 Base w , u ∈ 𝒫 Base w ⟼ z ∈ t LSSum ⁡ w u ⟼ ι x ∈ t | ∃ y ∈ u z = x + w y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpj1 class proj 1
1 vw setvar w
2 cvv class V
3 vt setvar t
4 cbs class Base
5 1 cv setvar w
6 5 4 cfv class Base w
7 6 cpw class 𝒫 Base w
8 vu setvar u
9 vz setvar z
10 3 cv setvar t
11 clsm class LSSum
12 5 11 cfv class LSSum ⁡ w
13 8 cv setvar u
14 10 13 12 co class t LSSum ⁡ w u
15 vx setvar x
16 vy setvar y
17 9 cv setvar z
18 15 cv setvar x
19 cplusg class + 𝑔
20 5 19 cfv class + w
21 16 cv setvar y
22 18 21 20 co class x + w y
23 17 22 wceq wff z = x + w y
24 23 16 13 wrex wff ∃ y ∈ u z = x + w y
25 24 15 10 crio class ι x ∈ t | ∃ y ∈ u z = x + w y
26 9 14 25 cmpt class z ∈ t LSSum ⁡ w u ⟼ ι x ∈ t | ∃ y ∈ u z = x + w y
27 3 8 7 7 26 cmpo class t ∈ 𝒫 Base w , u ∈ 𝒫 Base w ⟼ z ∈ t LSSum ⁡ w u ⟼ ι x ∈ t | ∃ y ∈ u z = x + w y
28 1 2 27 cmpt class w ∈ V ⟼ t ∈ 𝒫 Base w , u ∈ 𝒫 Base w ⟼ z ∈ t LSSum ⁡ w u ⟼ ι x ∈ t | ∃ y ∈ u z = x + w y
29 0 28 wceq wff proj 1 = w ∈ V ⟼ t ∈ 𝒫 Base w , u ∈ 𝒫 Base w ⟼ z ∈ t LSSum ⁡ w u ⟼ ι x ∈ t | ∃ y ∈ u z = x + w y