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

Definition df-lsm 18097
Description: Define subgroup sum (inner direct product of subgroups). (Contributed by NM, 28-Jan-2014.)
Assertion
Ref Expression
df-lsm LSSum = (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ ran (𝑥𝑡, 𝑦𝑢 ↦ (𝑥(+g𝑤)𝑦))))
Distinct variable group:   𝑤,𝑡,𝑢,𝑥,𝑦

Detailed syntax breakdown of Definition df-lsm
StepHypRef Expression
1 clsm 18095 . 2 class LSSum
2 vw . . 3 setvar 𝑤
3 cvv 3231 . . 3 class V
4 vt . . . 4 setvar 𝑡
5 vu . . . 4 setvar 𝑢
62cv 1522 . . . . . 6 class 𝑤
7 cbs 15904 . . . . . 6 class Base
86, 7cfv 5926 . . . . 5 class (Base‘𝑤)
98cpw 4191 . . . 4 class 𝒫 (Base‘𝑤)
10 vx . . . . . 6 setvar 𝑥
11 vy . . . . . 6 setvar 𝑦
124cv 1522 . . . . . 6 class 𝑡
135cv 1522 . . . . . 6 class 𝑢
1410cv 1522 . . . . . . 7 class 𝑥
1511cv 1522 . . . . . . 7 class 𝑦
16 cplusg 15988 . . . . . . . 8 class +g
176, 16cfv 5926 . . . . . . 7 class (+g𝑤)
1814, 15, 17co 6690 . . . . . 6 class (𝑥(+g𝑤)𝑦)
1910, 11, 12, 13, 18cmpt2 6692 . . . . 5 class (𝑥𝑡, 𝑦𝑢 ↦ (𝑥(+g𝑤)𝑦))
2019crn 5144 . . . 4 class ran (𝑥𝑡, 𝑦𝑢 ↦ (𝑥(+g𝑤)𝑦))
214, 5, 9, 9, 20cmpt2 6692 . . 3 class (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ ran (𝑥𝑡, 𝑦𝑢 ↦ (𝑥(+g𝑤)𝑦)))
222, 3, 21cmpt 4762 . 2 class (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ ran (𝑥𝑡, 𝑦𝑢 ↦ (𝑥(+g𝑤)𝑦))))
231, 22wceq 1523 1 wff LSSum = (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ ran (𝑥𝑡, 𝑦𝑢 ↦ (𝑥(+g𝑤)𝑦))))
Colors of variables: wff setvar class
This definition is referenced by:  lsmfval  18099
  Copyright terms: Public domain W3C validator