This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdsmm ⊢ ⊕m
1 vs ⊢ 𝑠
2 cvv ⊢ V
3 vr ⊢ 𝑟
4 1 cv ⊢ 𝑠
5 cprds ⊢ Xs
6 3 cv ⊢ 𝑟
7 4 6 5 co ⊢ ( 𝑠 Xs 𝑟 )
8 cress ⊢ ↾s
9 vf ⊢ 𝑓
10 vx ⊢ 𝑥
11 6 cdm ⊢ dom 𝑟
12 cbs ⊢ Base
13 10 cv ⊢ 𝑥
14 13 6 cfv ⊢ ( 𝑟 ‘ 𝑥 )
15 14 12 cfv ⊢ ( Base ‘ ( 𝑟 ‘ 𝑥 ) )
16 10 11 15 cixp ⊢ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) )
17 9 cv ⊢ 𝑓
18 13 17 cfv ⊢ ( 𝑓 ‘ 𝑥 )
19 c0g ⊢ 0g
20 14 19 cfv ⊢ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) )
21 18 20 wne ⊢ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) )
22 21 10 11 crab ⊢ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) }
23 cfn ⊢ Fin
24 22 23 wcel ⊢ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin
25 24 9 16 crab ⊢ { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin }
26 7 25 8 co ⊢ ( ( 𝑠 Xs 𝑟 ) ↾s { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } )
27 1 3 2 2 26 cmpo ⊢ ( 𝑠 ∈ V , 𝑟 ∈ V ↦ ( ( 𝑠 Xs 𝑟 ) ↾s { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } ) )
28 0 27 wceq ⊢ ⊕m = ( 𝑠 ∈ V , 𝑟 ∈ V ↦ ( ( 𝑠 Xs 𝑟 ) ↾s { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } ) )