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

Definition df-pj1 17968
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 17966 . 2 class proj1
2 vw . . 3 setvar 𝑤
3 cvv 3191 . . 3 class V
4 vt . . . 4 setvar 𝑡
5 vu . . . 4 setvar 𝑢
62cv 1479 . . . . . 6 class 𝑤
7 cbs 15776 . . . . . 6 class Base
86, 7cfv 5850 . . . . 5 class (Base‘𝑤)
98cpw 4135 . . . 4 class 𝒫 (Base‘𝑤)
10 vz . . . . 5 setvar 𝑧
114cv 1479 . . . . . 6 class 𝑡
125cv 1479 . . . . . 6 class 𝑢
13 clsm 17965 . . . . . . 7 class LSSum
146, 13cfv 5850 . . . . . 6 class (LSSum‘𝑤)
1511, 12, 14co 6605 . . . . 5 class (𝑡(LSSum‘𝑤)𝑢)
1610cv 1479 . . . . . . . 8 class 𝑧
17 vx . . . . . . . . . 10 setvar 𝑥
1817cv 1479 . . . . . . . . 9 class 𝑥
19 vy . . . . . . . . . 10 setvar 𝑦
2019cv 1479 . . . . . . . . 9 class 𝑦
21 cplusg 15857 . . . . . . . . . 10 class +g
226, 21cfv 5850 . . . . . . . . 9 class (+g𝑤)
2318, 20, 22co 6605 . . . . . . . 8 class (𝑥(+g𝑤)𝑦)
2416, 23wceq 1480 . . . . . . 7 wff 𝑧 = (𝑥(+g𝑤)𝑦)
2524, 19, 12wrex 2913 . . . . . 6 wff 𝑦𝑢 𝑧 = (𝑥(+g𝑤)𝑦)
2625, 17, 11crio 6565 . . . . 5 class (𝑥𝑡𝑦𝑢 𝑧 = (𝑥(+g𝑤)𝑦))
2710, 15, 26cmpt 4678 . . . 4 class (𝑧 ∈ (𝑡(LSSum‘𝑤)𝑢) ↦ (𝑥𝑡𝑦𝑢 𝑧 = (𝑥(+g𝑤)𝑦)))
284, 5, 9, 9, 27cmpt2 6607 . . 3 class (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ (𝑧 ∈ (𝑡(LSSum‘𝑤)𝑢) ↦ (𝑥𝑡𝑦𝑢 𝑧 = (𝑥(+g𝑤)𝑦))))
292, 3, 28cmpt 4678 . 2 class (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ (𝑧 ∈ (𝑡(LSSum‘𝑤)𝑢) ↦ (𝑥𝑡𝑦𝑢 𝑧 = (𝑥(+g𝑤)𝑦)))))
301, 29wceq 1480 1 wff proj1 = (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ (𝑧 ∈ (𝑡(LSSum‘𝑤)𝑢) ↦ (𝑥𝑡𝑦𝑢 𝑧 = (𝑥(+g𝑤)𝑦)))))
Colors of variables: wff setvar class
This definition is referenced by:  pj1fval  18023
  Copyright terms: Public domain W3C validator