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 = ( 𝑠 ∈ V , 𝑟 ∈ V ↦ ( ( 𝑠 Xs 𝑟 ) ↾s { 𝑓X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓𝑥 ) ≠ ( 0g ‘ ( 𝑟𝑥 ) ) } ∈ Fin } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdsmm m
1 vs 𝑠
2 cvv V
3 vr 𝑟
4 1 cv 𝑠
5 cprds Xs
6 3 cv 𝑟
7 4 6 5 co ( 𝑠 Xs 𝑟 )
8 cress s
9 vf 𝑓
10 vx 𝑥
11 6 cdm dom 𝑟
12 cbs Base
13 10 cv 𝑥
14 13 6 cfv ( 𝑟𝑥 )
15 14 12 cfv ( Base ‘ ( 𝑟𝑥 ) )
16 10 11 15 cixp X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟𝑥 ) )
17 9 cv 𝑓
18 13 17 cfv ( 𝑓𝑥 )
19 c0g 0g
20 14 19 cfv ( 0g ‘ ( 𝑟𝑥 ) )
21 18 20 wne ( 𝑓𝑥 ) ≠ ( 0g ‘ ( 𝑟𝑥 ) )
22 21 10 11 crab { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓𝑥 ) ≠ ( 0g ‘ ( 𝑟𝑥 ) ) }
23 cfn Fin
24 22 23 wcel { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓𝑥 ) ≠ ( 0g ‘ ( 𝑟𝑥 ) ) } ∈ Fin
25 24 9 16 crab { 𝑓X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓𝑥 ) ≠ ( 0g ‘ ( 𝑟𝑥 ) ) } ∈ Fin }
26 7 25 8 co ( ( 𝑠 Xs 𝑟 ) ↾s { 𝑓X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓𝑥 ) ≠ ( 0g ‘ ( 𝑟𝑥 ) ) } ∈ Fin } )
27 1 3 2 2 26 cmpo ( 𝑠 ∈ V , 𝑟 ∈ V ↦ ( ( 𝑠 Xs 𝑟 ) ↾s { 𝑓X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓𝑥 ) ≠ ( 0g ‘ ( 𝑟𝑥 ) ) } ∈ Fin } ) )
28 0 27 wceq m = ( 𝑠 ∈ V , 𝑟 ∈ V ↦ ( ( 𝑠 Xs 𝑟 ) ↾s { 𝑓X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓𝑥 ) ≠ ( 0g ‘ ( 𝑟𝑥 ) ) } ∈ Fin } ) )