Definition df-dsmm 21752

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

Distinct variable group:   𝑠,𝑟,𝑓,𝑥

Detailed syntax breakdown of Definition df-dsmm

Step	Hyp	Ref	Expression
1		cdsmm 21751	. 2 class ⊕m
2		vs	. . 3 setvar 𝑠
3		vr	. . 3 setvar 𝑟
4		cvv 3480	. . 3 class V
5	2	cv 1539	. . . . 5 class 𝑠
6	3	cv 1539	. . . . 5 class 𝑟
7		cprds 17490	. . . . 5 class Xs
8	5, 6, 7	co 7431	. . . 4 class (𝑠Xs𝑟)
9		vx	. . . . . . . . . 10 setvar 𝑥
10	9	cv 1539	. . . . . . . . 9 class 𝑥
11		vf	. . . . . . . . . 10 setvar 𝑓
12	11	cv 1539	. . . . . . . . 9 class 𝑓
13	10, 12	cfv 6561	. . . . . . . 8 class (𝑓‘𝑥)
14	10, 6	cfv 6561	. . . . . . . . 9 class (𝑟‘𝑥)
15		c0g 17484	. . . . . . . . 9 class 0g
16	14, 15	cfv 6561	. . . . . . . 8 class (0g‘(𝑟‘𝑥))
17	13, 16	wne 2940	. . . . . . 7 wff (𝑓‘𝑥) ≠ (0g‘(𝑟‘𝑥))
18	6	cdm 5685	. . . . . . 7 class dom 𝑟
19	17, 9, 18	crab 3436	. . . . . 6 class {𝑥 ∈ dom 𝑟 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑟‘𝑥))}
20		cfn 8985	. . . . . 6 class Fin
21	19, 20	wcel 2108	. . . . 5 wff {𝑥 ∈ dom 𝑟 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑟‘𝑥))} ∈ Fin
22		cbs 17247	. . . . . . 7 class Base
23	14, 22	cfv 6561	. . . . . 6 class (Base‘(𝑟‘𝑥))
24	9, 18, 23	cixp 8937	. . . . 5 class X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥))
25	21, 11, 24	crab 3436	. . . 4 class {𝑓 ∈ X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∣ {𝑥 ∈ dom 𝑟 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑟‘𝑥))} ∈ Fin}
26		cress 17274	. . . 4 class ↾s
27	8, 25, 26	co 7431	. . 3 class ((𝑠Xs𝑟) ↾s {𝑓 ∈ X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∣ {𝑥 ∈ dom 𝑟 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑟‘𝑥))} ∈ Fin})
28	2, 3, 4, 4, 27	cmpo 7433	. 2 class (𝑠 ∈ V, 𝑟 ∈ V ↦ ((𝑠Xs𝑟) ↾s {𝑓 ∈ X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∣ {𝑥 ∈ dom 𝑟 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑟‘𝑥))} ∈ Fin}))
29	1, 28	wceq 1540	1 wff ⊕m = (𝑠 ∈ V, 𝑟 ∈ V ↦ ((𝑠Xs𝑟) ↾s {𝑓 ∈ X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∣ {𝑥 ∈ dom 𝑟 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑟‘𝑥))} ∈ Fin}))

This definition is referenced by:  reldmdsmm  21753  dsmmval  21754