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

Definition df-dsmm 19895
 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 19894 . 2 class m
2 vs . . 3 setvar 𝑠
3 vr . . 3 setvar 𝑟
4 cvv 3173 . . 3 class V
52cv 1474 . . . . 5 class 𝑠
63cv 1474 . . . . 5 class 𝑟
7 cprds 15929 . . . . 5 class Xs
85, 6, 7co 6549 . . . 4 class (𝑠Xs𝑟)
9 vx . . . . . . . . . 10 setvar 𝑥
109cv 1474 . . . . . . . . 9 class 𝑥
11 vf . . . . . . . . . 10 setvar 𝑓
1211cv 1474 . . . . . . . . 9 class 𝑓
1310, 12cfv 5804 . . . . . . . 8 class (𝑓𝑥)
1410, 6cfv 5804 . . . . . . . . 9 class (𝑟𝑥)
15 c0g 15923 . . . . . . . . 9 class 0g
1614, 15cfv 5804 . . . . . . . 8 class (0g‘(𝑟𝑥))
1713, 16wne 2780 . . . . . . 7 wff (𝑓𝑥) ≠ (0g‘(𝑟𝑥))
186cdm 5038 . . . . . . 7 class dom 𝑟
1917, 9, 18crab 2900 . . . . . 6 class {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))}
20 cfn 7841 . . . . . 6 class Fin
2119, 20wcel 1977 . . . . 5 wff {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))} ∈ Fin
22 cbs 15695 . . . . . . 7 class Base
2314, 22cfv 5804 . . . . . 6 class (Base‘(𝑟𝑥))
249, 18, 23cixp 7794 . . . . 5 class X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥))
2521, 11, 24crab 2900 . . . 4 class {𝑓X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∣ {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))} ∈ Fin}
26 cress 15696 . . . 4 class s
278, 25, 26co 6549 . . 3 class ((𝑠Xs𝑟) ↾s {𝑓X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∣ {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))} ∈ Fin})
282, 3, 4, 4, 27cmpt2 6551 . 2 class (𝑠 ∈ V, 𝑟 ∈ V ↦ ((𝑠Xs𝑟) ↾s {𝑓X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∣ {𝑥 ∈ dom 𝑟 ∣ (𝑓𝑥) ≠ (0g‘(𝑟𝑥))} ∈ Fin}))
291, 28wceq 1475 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  19896  dsmmval  19897
 Copyright terms: Public domain W3C validator