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 } ) )