Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pj1 Structured version   Visualization version   GIF version

Definition df-pj1 18756
 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
StepHypRef Expression
1 cpj1 18754 . 2 class proj1
2 vw . . 3 setvar 𝑤
3 cvv 3495 . . 3 class V
4 vt . . . 4 setvar 𝑡
5 vu . . . 4 setvar 𝑢
62cv 1532 . . . . . 6 class 𝑤
7 cbs 16477 . . . . . 6 class Base
86, 7cfv 6350 . . . . 5 class (Base‘𝑤)
98cpw 4539 . . . 4 class 𝒫 (Base‘𝑤)
10 vz . . . . 5 setvar 𝑧
114cv 1532 . . . . . 6 class 𝑡
125cv 1532 . . . . . 6 class 𝑢
13 clsm 18753 . . . . . . 7 class LSSum
146, 13cfv 6350 . . . . . 6 class (LSSum‘𝑤)
1511, 12, 14co 7150 . . . . 5 class (𝑡(LSSum‘𝑤)𝑢)
1610cv 1532 . . . . . . . 8 class 𝑧
17 vx . . . . . . . . . 10 setvar 𝑥
1817cv 1532 . . . . . . . . 9 class 𝑥
19 vy . . . . . . . . . 10 setvar 𝑦
2019cv 1532 . . . . . . . . 9 class 𝑦
21 cplusg 16559 . . . . . . . . . 10 class +g
226, 21cfv 6350 . . . . . . . . 9 class (+g𝑤)
2318, 20, 22co 7150 . . . . . . . 8 class (𝑥(+g𝑤)𝑦)
2416, 23wceq 1533 . . . . . . 7 wff 𝑧 = (𝑥(+g𝑤)𝑦)
2524, 19, 12wrex 3139 . . . . . 6 wff 𝑦𝑢 𝑧 = (𝑥(+g𝑤)𝑦)
2625, 17, 11crio 7107 . . . . 5 class (𝑥𝑡𝑦𝑢 𝑧 = (𝑥(+g𝑤)𝑦))
2710, 15, 26cmpt 5139 . . . 4 class (𝑧 ∈ (𝑡(LSSum‘𝑤)𝑢) ↦ (𝑥𝑡𝑦𝑢 𝑧 = (𝑥(+g𝑤)𝑦)))
284, 5, 9, 9, 27cmpo 7152 . . 3 class (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ (𝑧 ∈ (𝑡(LSSum‘𝑤)𝑢) ↦ (𝑥𝑡𝑦𝑢 𝑧 = (𝑥(+g𝑤)𝑦))))
292, 3, 28cmpt 5139 . 2 class (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ (𝑧 ∈ (𝑡(LSSum‘𝑤)𝑢) ↦ (𝑥𝑡𝑦𝑢 𝑧 = (𝑥(+g𝑤)𝑦)))))
301, 29wceq 1533 1 wff proj1 = (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ (𝑧 ∈ (𝑡(LSSum‘𝑤)𝑢) ↦ (𝑥𝑡𝑦𝑢 𝑧 = (𝑥(+g𝑤)𝑦)))))
 Colors of variables: wff setvar class This definition is referenced by:  pj1fval  18814
 Copyright terms: Public domain W3C validator