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 e. _V |-> ( t e. ~P ( Base ` w ) , u e. ~P ( Base ` w ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` w ) y ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clsm 
 |-  LSSum
1 vw 
 |-  w
2 cvv 
 |-  _V
3 vt 
 |-  t
4 cbs 
 |-  Base
5 1 cv 
 |-  w
6 5 4 cfv 
 |-  ( Base ` w )
7 6 cpw 
 |-  ~P ( Base ` w )
8 vu 
 |-  u
9 vx 
 |-  x
10 3 cv 
 |-  t
11 vy 
 |-  y
12 8 cv 
 |-  u
13 9 cv 
 |-  x
14 cplusg 
 |-  +g
15 5 14 cfv 
 |-  ( +g ` w )
16 11 cv 
 |-  y
17 13 16 15 co 
 |-  ( x ( +g ` w ) y )
18 9 11 10 12 17 cmpo 
 |-  ( x e. t , y e. u |-> ( x ( +g ` w ) y ) )
19 18 crn 
 |-  ran ( x e. t , y e. u |-> ( x ( +g ` w ) y ) )
20 3 8 7 7 19 cmpo 
 |-  ( t e. ~P ( Base ` w ) , u e. ~P ( Base ` w ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` w ) y ) ) )
21 1 2 20 cmpt 
 |-  ( w e. _V |-> ( t e. ~P ( Base ` w ) , u e. ~P ( Base ` w ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` w ) y ) ) ) )
22 0 21 wceq 
 |-  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 ) ) ) )