# Metamath Proof Explorer

## Definition df-lsm

Description: Define subgroup sum (inner direct product of subgroups). (Contributed by NM, 28-Jan-2014)

Ref Expression
Assertion df-lsm ${⊢}\mathrm{LSSum}=\left({w}\in \mathrm{V}⟼\left({t}\in 𝒫{\mathrm{Base}}_{{w}},{u}\in 𝒫{\mathrm{Base}}_{{w}}⟼\mathrm{ran}\left({x}\in {t},{y}\in {u}⟼{x}{+}_{{w}}{y}\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 clsm ${class}\mathrm{LSSum}$
1 vw ${setvar}{w}$
2 cvv ${class}\mathrm{V}$
3 vt ${setvar}{t}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{w}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{w}}$
7 6 cpw ${class}𝒫{\mathrm{Base}}_{{w}}$
8 vu ${setvar}{u}$
9 vx ${setvar}{x}$
10 3 cv ${setvar}{t}$
11 vy ${setvar}{y}$
12 8 cv ${setvar}{u}$
13 9 cv ${setvar}{x}$
14 cplusg ${class}{+}_{𝑔}$
15 5 14 cfv ${class}{+}_{{w}}$
16 11 cv ${setvar}{y}$
17 13 16 15 co ${class}\left({x}{+}_{{w}}{y}\right)$
18 9 11 10 12 17 cmpo ${class}\left({x}\in {t},{y}\in {u}⟼{x}{+}_{{w}}{y}\right)$
19 18 crn ${class}\mathrm{ran}\left({x}\in {t},{y}\in {u}⟼{x}{+}_{{w}}{y}\right)$
20 3 8 7 7 19 cmpo ${class}\left({t}\in 𝒫{\mathrm{Base}}_{{w}},{u}\in 𝒫{\mathrm{Base}}_{{w}}⟼\mathrm{ran}\left({x}\in {t},{y}\in {u}⟼{x}{+}_{{w}}{y}\right)\right)$
21 1 2 20 cmpt ${class}\left({w}\in \mathrm{V}⟼\left({t}\in 𝒫{\mathrm{Base}}_{{w}},{u}\in 𝒫{\mathrm{Base}}_{{w}}⟼\mathrm{ran}\left({x}\in {t},{y}\in {u}⟼{x}{+}_{{w}}{y}\right)\right)\right)$
22 0 21 wceq ${wff}\mathrm{LSSum}=\left({w}\in \mathrm{V}⟼\left({t}\in 𝒫{\mathrm{Base}}_{{w}},{u}\in 𝒫{\mathrm{Base}}_{{w}}⟼\mathrm{ran}\left({x}\in {t},{y}\in {u}⟼{x}{+}_{{w}}{y}\right)\right)\right)$