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	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vt	$$setvart$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarw$$
6	5 4	cfv	$$class{\mathrm{Base}}_w$$
7	6	cpw	$$class𝒫{\mathrm{Base}}_w$$
8		vu	$$setvaru$$
9		vx	$$setvarx$$
10	3	cv	$$setvart$$
11		vy	$$setvary$$
12	8	cv	$$setvaru$$
13	9	cv	$$setvarx$$
14		cplusg	$$class{+}_{𝑔}$$
15	5 14	cfv	$$class{+}_w$$
16	11	cv	$$setvary$$
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)$$