Definition df-lsm 19654

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

Step	Hyp	Ref	Expression
1		clsm 19652	. 2 class LSSum
2		vw	. . 3 setvar 𝑤
3		cvv 3480	. . 3 class V
4		vt	. . . 4 setvar 𝑡
5		vu	. . . 4 setvar 𝑢
6	2	cv 1539	. . . . . 6 class 𝑤
7		cbs 17247	. . . . . 6 class Base
8	6, 7	cfv 6561	. . . . 5 class (Base‘𝑤)
9	8	cpw 4600	. . . 4 class 𝒫 (Base‘𝑤)
10		vx	. . . . . 6 setvar 𝑥
11		vy	. . . . . 6 setvar 𝑦
12	4	cv 1539	. . . . . 6 class 𝑡
13	5	cv 1539	. . . . . 6 class 𝑢
14	10	cv 1539	. . . . . . 7 class 𝑥
15	11	cv 1539	. . . . . . 7 class 𝑦
16		cplusg 17297	. . . . . . . 8 class +g
17	6, 16	cfv 6561	. . . . . . 7 class (+g‘𝑤)
18	14, 15, 17	co 7431	. . . . . 6 class (𝑥(+g‘𝑤)𝑦)
19	10, 11, 12, 13, 18	cmpo 7433	. . . . 5 class (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑤)𝑦))
20	19	crn 5686	. . . 4 class ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑤)𝑦))
21	4, 5, 9, 9, 20	cmpo 7433	. . 3 class (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑤)𝑦)))
22	2, 3, 21	cmpt 5225	. 2 class (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑤)𝑦))))
23	1, 22	wceq 1540	1 wff LSSum = (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑤)𝑦))))

This definition is referenced by:  lsmfval  19656