This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-dsmm

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)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdsmm 
 |-  (+)m
1 vs 
 |-  s
2 cvv 
 |-  _V
3 vr 
 |-  r
4 1 cv 
 |-  s
5 cprds 
 |-  Xs_
6 3 cv 
 |-  r
7 4 6 5 co 
 |-  ( s Xs_ r )
8 cress 
 |-  |`s
9 vf 
 |-  f
10 vx 
 |-  x
11 6 cdm 
 |-  dom r
12 cbs 
 |-  Base
13 10 cv 
 |-  x
14 13 6 cfv 
 |-  ( r ` x )
15 14 12 cfv 
 |-  ( Base ` ( r ` x ) )
16 10 11 15 cixp 
 |-  X_ x e. dom r ( Base ` ( r ` x ) )
17 9 cv 
 |-  f
18 13 17 cfv 
 |-  ( f ` x )
19 c0g 
 |-  0g
20 14 19 cfv 
 |-  ( 0g ` ( r ` x ) )
21 18 20 wne 
 |-  ( f ` x ) =/= ( 0g ` ( r ` x ) )
22 21 10 11 crab 
 |-  { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) }
23 cfn 
 |-  Fin
24 22 23 wcel 
 |-  { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin
25 24 9 16 crab 
 |-  { f e. X_ x e. dom r ( Base ` ( r ` x ) ) | { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin }
26 7 25 8 co 
 |-  ( ( s Xs_ r ) |`s { f e. X_ x e. dom r ( Base ` ( r ` x ) ) | { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin } )
27 1 3 2 2 26 cmpo 
 |-  ( s e. _V , r e. _V |-> ( ( s Xs_ r ) |`s { f e. X_ x e. dom r ( Base ` ( r ` x ) ) | { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin } ) )
28 0 27 wceq 
 |-  (+)m = ( s e. _V , r e. _V |-> ( ( s Xs_ r ) |`s { f e. X_ x e. dom r ( Base ` ( r ` x ) ) | { x e. dom r | ( f ` x ) =/= ( 0g ` ( r ` x ) ) } e. Fin } ) )