Definition df-lsm 18051

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

Assertion

Ref	Expression
df-lsm	|- LSSum = ( w e. _V |-> ( t e. ~P ( Base ` w ) , u e. ~P ( Base ` w ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` w ) y ) ) ) )

Distinct variable group:   w, t, u, x, y

Detailed syntax breakdown of Definition df-lsm

Step	Hyp	Ref	Expression
1		clsm 18049	. 2 class LSSum
2		vw	. . 3 setvar w
3		cvv 3200	. . 3 class _V
4		vt	. . . 4 setvar t
5		vu	. . . 4 setvar u
6	2	cv 1482	. . . . . 6 class w
7		cbs 15857	. . . . . 6 class Base
8	6, 7	cfv 5888	. . . . 5 class ( Base ` w )
9	8	cpw 4158	. . . 4 class ~P ( Base ` w )
10		vx	. . . . . 6 setvar x
11		vy	. . . . . 6 setvar y
12	4	cv 1482	. . . . . 6 class t
13	5	cv 1482	. . . . . 6 class u
14	10	cv 1482	. . . . . . 7 class x
15	11	cv 1482	. . . . . . 7 class y
16		cplusg 15941	. . . . . . . 8 class +g
17	6, 16	cfv 5888	. . . . . . 7 class ( +g ` w )
18	14, 15, 17	co 6650	. . . . . 6 class ( x ( +g ` w ) y )
19	10, 11, 12, 13, 18	cmpt2 6652	. . . . 5 class ( x e. t , y e. u |-> ( x ( +g ` w ) y ) )
20	19	crn 5115	. . . 4 class ran ( x e. t , y e. u |-> ( x ( +g ` w ) y ) )
21	4, 5, 9, 9, 20	cmpt2 6652	. . 3 class ( t e. ~P ( Base ` w ) , u e. ~P ( Base ` w ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` w ) y ) ) )
22	2, 3, 21	cmpt 4729	. 2 class ( w e. _V |-> ( t e. ~P ( Base ` w ) , u e. ~P ( Base ` w ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` w ) y ) ) ) )
23	1, 22	wceq 1483	1 wff LSSum = ( w e. _V |-> ( t e. ~P ( Base ` w ) , u e. ~P ( Base ` w ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` w ) y ) ) ) )

This definition is referenced by:  lsmfval  18053