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 ∈ V , r ∈ V ⟼ s ⨉ 𝑠 r ↾ 𝑠 f ∈ ⨉ x ∈ dom ⁡ r Base r ⁡ x | x ∈ dom ⁡ r | f ⁡ x ≠ 0 r ⁡ x ∈ Fin

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdsmm class ⊕ m
1 vs setvar s
2 cvv class V
3 vr setvar r
4 1 cv setvar s
5 cprds class ⨉ 𝑠
6 3 cv setvar r
7 4 6 5 co class s ⨉ 𝑠 r
8 cress class ↾ 𝑠
9 vf setvar f
10 vx setvar x
11 6 cdm class dom ⁡ r
12 cbs class Base
13 10 cv setvar x
14 13 6 cfv class r ⁡ x
15 14 12 cfv class Base r ⁡ x
16 10 11 15 cixp class ⨉ x ∈ dom ⁡ r Base r ⁡ x
17 9 cv setvar f
18 13 17 cfv class f ⁡ x
19 c0g class 0 𝑔
20 14 19 cfv class 0 r ⁡ x
21 18 20 wne wff f ⁡ x ≠ 0 r ⁡ x
22 21 10 11 crab class x ∈ dom ⁡ r | f ⁡ x ≠ 0 r ⁡ x
23 cfn class Fin
24 22 23 wcel wff x ∈ dom ⁡ r | f ⁡ x ≠ 0 r ⁡ x ∈ Fin
25 24 9 16 crab class f ∈ ⨉ x ∈ dom ⁡ r Base r ⁡ x | x ∈ dom ⁡ r | f ⁡ x ≠ 0 r ⁡ x ∈ Fin
26 7 25 8 co class s ⨉ 𝑠 r ↾ 𝑠 f ∈ ⨉ x ∈ dom ⁡ r Base r ⁡ x | x ∈ dom ⁡ r | f ⁡ x ≠ 0 r ⁡ x ∈ Fin
27 1 3 2 2 26 cmpo class s ∈ V , r ∈ V ⟼ s ⨉ 𝑠 r ↾ 𝑠 f ∈ ⨉ x ∈ dom ⁡ r Base r ⁡ x | x ∈ dom ⁡ r | f ⁡ x ≠ 0 r ⁡ x ∈ Fin
28 0 27 wceq wff ⊕ m = s ∈ V , r ∈ V ⟼ s ⨉ 𝑠 r ↾ 𝑠 f ∈ ⨉ x ∈ dom ⁡ r Base r ⁡ x | x ∈ dom ⁡ r | f ⁡ x ≠ 0 r ⁡ x ∈ Fin