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 17972
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 17970 . 2 class LSSum
2 vw . . 3 setvar 𝑤
3 cvv 3186 . . 3 class V
4 vt . . . 4 setvar 𝑡
5 vu . . . 4 setvar 𝑢
62cv 1479 . . . . . 6 class 𝑤
7 cbs 15781 . . . . . 6 class Base
86, 7cfv 5847 . . . . 5 class (Base‘𝑤)
98cpw 4130 . . . 4 class 𝒫 (Base‘𝑤)
10 vx . . . . . 6 setvar 𝑥
11 vy . . . . . 6 setvar 𝑦
124cv 1479 . . . . . 6 class 𝑡
135cv 1479 . . . . . 6 class 𝑢
1410cv 1479 . . . . . . 7 class 𝑥
1511cv 1479 . . . . . . 7 class 𝑦
16 cplusg 15862 . . . . . . . 8 class +g
176, 16cfv 5847 . . . . . . 7 class (+g𝑤)
1814, 15, 17co 6604 . . . . . 6 class (𝑥(+g𝑤)𝑦)
1910, 11, 12, 13, 18cmpt2 6606 . . . . 5 class (𝑥𝑡, 𝑦𝑢 ↦ (𝑥(+g𝑤)𝑦))
2019crn 5075 . . . 4 class ran (𝑥𝑡, 𝑦𝑢 ↦ (𝑥(+g𝑤)𝑦))
214, 5, 9, 9, 20cmpt2 6606 . . 3 class (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ ran (𝑥𝑡, 𝑦𝑢 ↦ (𝑥(+g𝑤)𝑦)))
222, 3, 21cmpt 4673 . 2 class (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ ran (𝑥𝑡, 𝑦𝑢 ↦ (𝑥(+g𝑤)𝑦))))
231, 22wceq 1480 1 wff LSSum = (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ ran (𝑥𝑡, 𝑦𝑢 ↦ (𝑥(+g𝑤)𝑦))))
Colors of variables: wff setvar class
This definition is referenced by:  lsmfval  17974
  Copyright terms: Public domain W3C validator