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	$⊢ \oplus_{m} = (s \in V, r \in V ⟼ (s ⨉_{𝑠} r) ↾_{𝑠} \{f \in \underset{x \in dom r}{⨉} {Base}_{r (x)} \| \{x \in dom r \| f (x) \neq 0_{r (x)}\} \in Fin\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdsmm	$class \oplus_{m}$
1		vs	$setvar s$
2		cvv	$class V$
3		vr	$setvar r$
4	1	cv	$setvar s$
5		cprds	$class ⨉_{𝑠}$
6	3	cv	$setvar r$
7	4 6 5	co	$class (s ⨉_{𝑠} r)$
8		cress	$class ↾_{𝑠}$
9		vf	$setvar f$
10		vx	$setvar x$
11	6	cdm	$class dom r$
12		cbs	$class Base$
13	10	cv	$setvar x$
14	13 6	cfv	$class r (x)$
15	14 12	cfv	$class {Base}_{r (x)}$
16	10 11 15	cixp	$class \underset{x \in dom r}{⨉} {Base}_{r (x)}$
17	9	cv	$setvar f$
18	13 17	cfv	$class f (x)$
19		c0g	$class 0_{𝑔}$
20	14 19	cfv	$class 0_{r (x)}$
21	18 20	wne	$wff f (x) \neq 0_{r (x)}$
22	21 10 11	crab	$class \{x \in dom r \| f (x) \neq 0_{r (x)}\}$
23		cfn	$class Fin$
24	22 23	wcel	$wff \{x \in dom r \| f (x) \neq 0_{r (x)}\} \in Fin$
25	24 9 16	crab	$class \{f \in \underset{x \in dom r}{⨉} {Base}_{r (x)} \| \{x \in dom r \| f (x) \neq 0_{r (x)}\} \in Fin\}$
26	7 25 8	co	$class ((s ⨉_{𝑠} r) ↾_{𝑠} \{f \in \underset{x \in dom r}{⨉} {Base}_{r (x)} \| \{x \in dom r \| f (x) \neq 0_{r (x)}\} \in Fin\})$
27	1 3 2 2 26	cmpo	$class (s \in V, r \in V ⟼ (s ⨉_{𝑠} r) ↾_{𝑠} \{f \in \underset{x \in dom r}{⨉} {Base}_{r (x)} \| \{x \in dom r \| f (x) \neq 0_{r (x)}\} \in Fin\})$
28	0 27	wceq	$wff \oplus_{m} = (s \in V, r \in V ⟼ (s ⨉_{𝑠} r) ↾_{𝑠} \{f \in \underset{x \in dom r}{⨉} {Base}_{r (x)} \| \{x \in dom r \| f (x) \neq 0_{r (x)}\} \in Fin\})$

Metamath Proof Explorer

Definition df-dsmm

Detailed syntax breakdown