MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dsmm Structured version   Visualization version   GIF version

Definition df-dsmm 19834
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
StepHypRef Expression
1 cdsmm 19833 . 2 class m
2 vs . . 3 setvar 𝑠
3 vr . . 3 setvar 𝑟
4 cvv 3169 . . 3 class V
52cv 1473 . . . . 5 class 𝑠
63cv 1473 . . . . 5 class 𝑟
7 cprds 15872 . . . . 5 class Xs
85, 6, 7co 6524 . . . 4 class (𝑠Xs𝑟)
9 vx . . . . . . . . . 10 setvar 𝑥
109cv 1473 . . . . . . . . 9 class 𝑥
11 vf . . . . . . . . . 10 setvar 𝑓
1211cv 1473 . . . . . . . . 9 class 𝑓
1310, 12cfv 5787 . . . . . . . 8 class (𝑓𝑥)
1410, 6cfv 5787 . . . . . . . . 9 class (𝑟𝑥)
15 c0g 15866 . . . . . . . . 9 class 0g
1614, 15cfv 5787 . . . . . . . 8 class (0g‘(𝑟𝑥))
1713, 16wne 2776 . . . . . . 7 wff (𝑓𝑥) ≠ (0g‘(𝑟𝑥))
186cdm 5025 . . . . . . 7 class dom 𝑟
1917, 9, 18crab 2896 . . . . . 6 class {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))}
20 cfn 7815 . . . . . 6 class Fin
2119, 20wcel 1976 . . . . 5 wff {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))} ∈ Fin
22 cbs 15638 . . . . . . 7 class Base
2314, 22cfv 5787 . . . . . 6 class (Base‘(𝑟𝑥))
249, 18, 23cixp 7768 . . . . 5 class X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥))
2521, 11, 24crab 2896 . . . 4 class {𝑓X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∣ {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))} ∈ Fin}
26 cress 15639 . . . 4 class s
278, 25, 26co 6524 . . 3 class ((𝑠Xs𝑟) ↾s {𝑓X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∣ {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))} ∈ Fin})
282, 3, 4, 4, 27cmpt2 6526 . 2 class (𝑠 ∈ V, 𝑟 ∈ V ↦ ((𝑠Xs𝑟) ↾s {𝑓X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∣ {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))} ∈ Fin}))
291, 28wceq 1474 1 wff m = (𝑠 ∈ V, 𝑟 ∈ V ↦ ((𝑠Xs𝑟) ↾s {𝑓X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∣ {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))} ∈ Fin}))
Colors of variables: wff setvar class
This definition is referenced by:  reldmdsmm  19835  dsmmval  19836
  Copyright terms: Public domain W3C validator