Definition df-dsmm 20076

Description: The direct sum of a family of Abelian groups or left modules is the induced group structure on finite linear combinations of elements, here represented as functions with finite support. (Contributed by Stefan O'Rear, 7-Jan-2015.)

Assertion

Ref	Expression
df-dsmm	|- (+)m = ( s e. _V , r e. _V |-> ( ( s X_s r ) ↾s { f e. X_ x e. dom r ( Base ` ( r ` x ) ) | { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin } ) )

Distinct variable group:   s, r, f, x

Detailed syntax breakdown of Definition df-dsmm

Step	Hyp	Ref	Expression
1		cdsmm 20075	. 2 class (+)m
2		vs	. . 3 setvar s
3		vr	. . 3 setvar r
4		cvv 3200	. . 3 class _V
5	2	cv 1482	. . . . 5 class s
6	3	cv 1482	. . . . 5 class r
7		cprds 16106	. . . . 5 class X_s
8	5, 6, 7	co 6650	. . . 4 class ( s X_s r )
9		vx	. . . . . . . . . 10 setvar x
10	9	cv 1482	. . . . . . . . 9 class x
11		vf	. . . . . . . . . 10 setvar f
12	11	cv 1482	. . . . . . . . 9 class f
13	10, 12	cfv 5888	. . . . . . . 8 class ( f ` x )
14	10, 6	cfv 5888	. . . . . . . . 9 class ( r ` x )
15		c0g 16100	. . . . . . . . 9 class 0g
16	14, 15	cfv 5888	. . . . . . . 8 class ( 0g ` ( r ` x ) )
17	13, 16	wne 2794	. . . . . . 7 wff ( f ` x ) =/= ( 0g ` ( r ` x ) )
18	6	cdm 5114	. . . . . . 7 class dom r
19	17, 9, 18	crab 2916	. . . . . 6 class { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) }
20		cfn 7955	. . . . . 6 class Fin
21	19, 20	wcel 1990	. . . . 5 wff { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin
22		cbs 15857	. . . . . . 7 class Base
23	14, 22	cfv 5888	. . . . . 6 class ( Base ` ( r ` x ) )
24	9, 18, 23	cixp 7908	. . . . 5 class X_ x e. dom r ( Base ` ( r ` x ) )
25	21, 11, 24	crab 2916	. . . 4 class { f e. X_ x e. dom r ( Base ` ( r ` x ) ) | { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin }
26		cress 15858	. . . 4 class ↾s
27	8, 25, 26	co 6650	. . 3 class ( ( s X_s r ) ↾s { f e. X_ x e. dom r ( Base ` ( r ` x ) ) | { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin } )
28	2, 3, 4, 4, 27	cmpt2 6652	. 2 class ( s e. _V , r e. _V |-> ( ( s X_s r ) ↾s { f e. X_ x e. dom r ( Base ` ( r ` x ) ) | { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin } ) )
29	1, 28	wceq 1483	1 wff (+)m = ( s e. _V , r e. _V |-> ( ( s X_s r ) ↾s { f e. X_ x e. dom r ( Base ` ( r ` x ) ) | { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin } ) )

This definition is referenced by:  reldmdsmm  20077  dsmmval  20078