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 20806
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 20805 . 2 class m
2 vs . . 3 setvar 𝑠
3 vr . . 3 setvar 𝑟
4 cvv 3495 . . 3 class V
52cv 1527 . . . . 5 class 𝑠
63cv 1527 . . . . 5 class 𝑟
7 cprds 16709 . . . . 5 class Xs
85, 6, 7co 7145 . . . 4 class (𝑠Xs𝑟)
9 vx . . . . . . . . . 10 setvar 𝑥
109cv 1527 . . . . . . . . 9 class 𝑥
11 vf . . . . . . . . . 10 setvar 𝑓
1211cv 1527 . . . . . . . . 9 class 𝑓
1310, 12cfv 6349 . . . . . . . 8 class (𝑓𝑥)
1410, 6cfv 6349 . . . . . . . . 9 class (𝑟𝑥)
15 c0g 16703 . . . . . . . . 9 class 0g
1614, 15cfv 6349 . . . . . . . 8 class (0g‘(𝑟𝑥))
1713, 16wne 3016 . . . . . . 7 wff (𝑓𝑥) ≠ (0g‘(𝑟𝑥))
186cdm 5549 . . . . . . 7 class dom 𝑟
1917, 9, 18crab 3142 . . . . . 6 class {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))}
20 cfn 8498 . . . . . 6 class Fin
2119, 20wcel 2105 . . . . 5 wff {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))} ∈ Fin
22 cbs 16473 . . . . . . 7 class Base
2314, 22cfv 6349 . . . . . 6 class (Base‘(𝑟𝑥))
249, 18, 23cixp 8450 . . . . 5 class X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥))
2521, 11, 24crab 3142 . . . 4 class {𝑓X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∣ {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))} ∈ Fin}
26 cress 16474 . . . 4 class s
278, 25, 26co 7145 . . 3 class ((𝑠Xs𝑟) ↾s {𝑓X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∣ {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))} ∈ Fin})
282, 3, 4, 4, 27cmpo 7147 . 2 class (𝑠 ∈ V, 𝑟 ∈ V ↦ ((𝑠Xs𝑟) ↾s {𝑓X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∣ {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))} ∈ Fin}))
291, 28wceq 1528 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  20807  dsmmval  20808
  Copyright terms: Public domain W3C validator