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 LSSum = w V t 𝒫 Base w , u 𝒫 Base w ran x t , y u x + w y

Detailed syntax breakdown

Step Hyp Ref Expression
0 clsm class LSSum
1 vw setvar w
2 cvv class V
3 vt setvar t
4 cbs class Base
5 1 cv setvar w
6 5 4 cfv class Base w
7 6 cpw class 𝒫 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 x + w y
18 9 11 10 12 17 cmpo class x t , y u x + w y
19 18 crn class ran x t , y u x + w y
20 3 8 7 7 19 cmpo class t 𝒫 Base w , u 𝒫 Base w ran x t , y u x + w y
21 1 2 20 cmpt class w V t 𝒫 Base w , u 𝒫 Base w ran x t , y u x + w y
22 0 21 wceq wff LSSum = w V t 𝒫 Base w , u 𝒫 Base w ran x t , y u x + w y