dsmmval

Description: Value of the module direct sum. (Contributed by Stefan O'Rear, 7-Jan-2015)

		Ref	Expression
	Hypothesis	dsmmval.b	$⊢ B = \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\}$
	Assertion	dsmmval	$⊢ R \in V \to S \oplus_{m} R = (S ⨉_{𝑠} R) ↾_{𝑠} B$

Proof

Step	Hyp	Ref	Expression
1		dsmmval.b	$⊢ B = \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\}$
2		elex	$⊢ R \in V \to R \in V$
3		oveq12	$⊢ (s = S \land r = R) \to s ⨉_{𝑠} r = S ⨉_{𝑠} R$
4		eqid	$⊢ s ⨉_{𝑠} r = s ⨉_{𝑠} r$
5		vex	$⊢ s \in V$
6	5	a1i	$⊢ (s = S \land r = R) \to s \in V$
7		vex	$⊢ r \in V$
8	7	a1i	$⊢ (s = S \land r = R) \to r \in V$
9		eqid	$⊢ {Base}_{(s ⨉_{𝑠} r)} = {Base}_{(s ⨉_{𝑠} r)}$
10		eqidd	$⊢ (s = S \land r = R) \to dom r = dom r$
11	4 6 8 9 10	prdsbas	$⊢ (s = S \land r = R) \to {Base}_{(s ⨉_{𝑠} r)} = \underset{x \in dom r}{⨉} {Base}_{r (x)}$
12	3	fveq2d	$⊢ (s = S \land r = R) \to {Base}_{(s ⨉_{𝑠} r)} = {Base}_{(S ⨉_{𝑠} R)}$
13	11 12	eqtr3d	$⊢ (s = S \land r = R) \to \underset{x \in dom r}{⨉} {Base}_{r (x)} = {Base}_{(S ⨉_{𝑠} R)}$
14		simpr	$⊢ (s = S \land r = R) \to r = R$
15	14	dmeqd	$⊢ (s = S \land r = R) \to dom r = dom R$
16	14	fveq1d	$⊢ (s = S \land r = R) \to r (x) = R (x)$
17	16	fveq2d	$⊢ (s = S \land r = R) \to 0_{r (x)} = 0_{R (x)}$
18	17	neeq2d	$⊢ (s = S \land r = R) \to (f (x) \neq 0_{r (x)} \leftrightarrow f (x) \neq 0_{R (x)})$
19	15 18	rabeqbidv	$⊢ (s = S \land r = R) \to \{x \in dom r \| f (x) \neq 0_{r (x)}\} = \{x \in dom R \| f (x) \neq 0_{R (x)}\}$
20	19	eleq1d	$⊢ (s = S \land r = R) \to (\{x \in dom r \| f (x) \neq 0_{r (x)}\} \in Fin \leftrightarrow \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin)$
21	13 20	rabeqbidv	$⊢ (s = S \land r = R) \to \{f \in \underset{x \in dom r}{⨉} {Base}_{r (x)} \| \{x \in dom r \| f (x) \neq 0_{r (x)}\} \in Fin\} = \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\}$
22	21 1	eqtr4di	$⊢ (s = S \land r = R) \to \{f \in \underset{x \in dom r}{⨉} {Base}_{r (x)} \| \{x \in dom r \| f (x) \neq 0_{r (x)}\} \in Fin\} = B$
23	3 22	oveq12d	$⊢ (s = S \land r = R) \to (s ⨉_{𝑠} r) ↾_{𝑠} \{f \in \underset{x \in dom r}{⨉} {Base}_{r (x)} \| \{x \in dom r \| f (x) \neq 0_{r (x)}\} \in Fin\} = (S ⨉_{𝑠} R) ↾_{𝑠} B$
24		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\})$
25		ovex	$⊢ (S ⨉_{𝑠} R) ↾_{𝑠} B \in V$
26	23 24 25	ovmpoa	$⊢ (S \in V \land R \in V) \to S \oplus_{m} R = (S ⨉_{𝑠} R) ↾_{𝑠} B$
27		reldmdsmm	$⊢ Rel dom \oplus_{m}$
28	27	ovprc1	$⊢ \neg S \in V \to S \oplus_{m} R = \emptyset$
29		ress0	$⊢ \emptyset ↾_{𝑠} B = \emptyset$
30	28 29	eqtr4di	$⊢ \neg S \in V \to S \oplus_{m} R = \emptyset ↾_{𝑠} B$
31		reldmprds	$⊢ Rel dom ⨉_{𝑠}$
32	31	ovprc1	$⊢ \neg S \in V \to S ⨉_{𝑠} R = \emptyset$
33	32	oveq1d	$⊢ \neg S \in V \to (S ⨉_{𝑠} R) ↾_{𝑠} B = \emptyset ↾_{𝑠} B$
34	30 33	eqtr4d	$⊢ \neg S \in V \to S \oplus_{m} R = (S ⨉_{𝑠} R) ↾_{𝑠} B$
35	34	adantr	$⊢ (\neg S \in V \land R \in V) \to S \oplus_{m} R = (S ⨉_{𝑠} R) ↾_{𝑠} B$
36	26 35	pm2.61ian	$⊢ R \in V \to S \oplus_{m} R = (S ⨉_{𝑠} R) ↾_{𝑠} B$
37	2 36	syl	$⊢ R \in V \to S \oplus_{m} R = (S ⨉_{𝑠} R) ↾_{𝑠} B$

Metamath Proof Explorer

Theorem dsmmval

Proof