MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lsm Unicode version

Definition df-lsm 14947
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
StepHypRef Expression
1 clsm 14945 . 2  class  LSSum
2 vw . . 3  set  w
3 cvv 2788 . . 3  class  _V
4 vt . . . 4  set  t
5 vu . . . 4  set  u
62cv 1622 . . . . . 6  class  w
7 cbs 13148 . . . . . 6  class  Base
86, 7cfv 5255 . . . . 5  class  ( Base `  w )
98cpw 3625 . . . 4  class  ~P ( Base `  w )
10 vx . . . . . 6  set  x
11 vy . . . . . 6  set  y
124cv 1622 . . . . . 6  class  t
135cv 1622 . . . . . 6  class  u
1410cv 1622 . . . . . . 7  class  x
1511cv 1622 . . . . . . 7  class  y
16 cplusg 13208 . . . . . . . 8  class  +g
176, 16cfv 5255 . . . . . . 7  class  ( +g  `  w )
1814, 15, 17co 5858 . . . . . 6  class  ( x ( +g  `  w
) y )
1910, 11, 12, 13, 18cmpt2 5860 . . . . 5  class  ( x  e.  t ,  y  e.  u  |->  ( x ( +g  `  w
) y ) )
2019crn 4690 . . . 4  class  ran  (
x  e.  t ,  y  e.  u  |->  ( x ( +g  `  w
) y ) )
214, 5, 9, 9, 20cmpt2 5860 . . 3  class  ( t  e.  ~P ( Base `  w ) ,  u  e.  ~P ( Base `  w
)  |->  ran  ( x  e.  t ,  y  e.  u  |->  ( x ( +g  `  w ) y ) ) )
222, 3, 21cmpt 4077 . 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 ) ) ) )
231, 22wceq 1623 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 ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  lsmfval  14949
  Copyright terms: Public domain W3C validator