dsmmval2

Description: Self-referential definition of the module direct sum. (Contributed by Stefan O'Rear, 7-Jan-2015) (Revised by Stefan O'Rear, 6-May-2015)

		Ref	Expression
	Hypothesis	dsmmval2.b	$⊢ B = {Base}_{(S \oplus_{m} R)}$
	Assertion	dsmmval2	$⊢ S \oplus_{m} R = (S ⨉_{𝑠} R) ↾_{𝑠} B$

Proof

Step	Hyp	Ref	Expression
1		dsmmval2.b	$⊢ B = {Base}_{(S \oplus_{m} R)}$
2		ssrab2	$⊢ \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\} \subseteq {Base}_{(S ⨉_{𝑠} R)}$
3		eqid	$⊢ (S ⨉_{𝑠} R) ↾_{𝑠} \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\} = (S ⨉_{𝑠} R) ↾_{𝑠} \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\}$
4		eqid	$⊢ {Base}_{(S ⨉_{𝑠} R)} = {Base}_{(S ⨉_{𝑠} R)}$
5	3 4	ressbas2	$⊢ \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\} \subseteq {Base}_{(S ⨉_{𝑠} R)} \to \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\} = {Base}_{((S ⨉_{𝑠} R) ↾_{𝑠} \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\})}$
6	2 5	ax-mp	$⊢ \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\} = {Base}_{((S ⨉_{𝑠} R) ↾_{𝑠} \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\})}$
7	6	oveq2i	$⊢ (S ⨉_{𝑠} R) ↾_{𝑠} \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\} = (S ⨉_{𝑠} R) ↾_{𝑠} {Base}_{((S ⨉_{𝑠} R) ↾_{𝑠} \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\})}$
8		eqid	$⊢ \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{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\}$
9	8	dsmmval	$⊢ R \in V \to S \oplus_{m} R = (S ⨉_{𝑠} R) ↾_{𝑠} \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\}$
10	9	fveq2d	$⊢ R \in V \to {Base}_{(S \oplus_{m} R)} = {Base}_{((S ⨉_{𝑠} R) ↾_{𝑠} \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\})}$
11	10	oveq2d	$⊢ R \in V \to (S ⨉_{𝑠} R) ↾_{𝑠} {Base}_{(S \oplus_{m} R)} = (S ⨉_{𝑠} R) ↾_{𝑠} {Base}_{((S ⨉_{𝑠} R) ↾_{𝑠} \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\})}$
12	7 9 11	3eqtr4a	$⊢ R \in V \to S \oplus_{m} R = (S ⨉_{𝑠} R) ↾_{𝑠} {Base}_{(S \oplus_{m} R)}$
13		ress0	$⊢ \emptyset ↾_{𝑠} {Base}_{(S \oplus_{m} R)} = \emptyset$
14	13	eqcomi	$⊢ \emptyset = \emptyset ↾_{𝑠} {Base}_{(S \oplus_{m} R)}$
15		reldmdsmm	$⊢ Rel dom \oplus_{m}$
16	15	ovprc2	$⊢ \neg R \in V \to S \oplus_{m} R = \emptyset$
17		reldmprds	$⊢ Rel dom ⨉_{𝑠}$
18	17	ovprc2	$⊢ \neg R \in V \to S ⨉_{𝑠} R = \emptyset$
19	18	oveq1d	$⊢ \neg R \in V \to (S ⨉_{𝑠} R) ↾_{𝑠} {Base}_{(S \oplus_{m} R)} = \emptyset ↾_{𝑠} {Base}_{(S \oplus_{m} R)}$
20	14 16 19	3eqtr4a	$⊢ \neg R \in V \to S \oplus_{m} R = (S ⨉_{𝑠} R) ↾_{𝑠} {Base}_{(S \oplus_{m} R)}$
21	12 20	pm2.61i	$⊢ S \oplus_{m} R = (S ⨉_{𝑠} R) ↾_{𝑠} {Base}_{(S \oplus_{m} R)}$
22	1	oveq2i	$⊢ (S ⨉_{𝑠} R) ↾_{𝑠} B = (S ⨉_{𝑠} R) ↾_{𝑠} {Base}_{(S \oplus_{m} R)}$
23	21 22	eqtr4i	$⊢ S \oplus_{m} R = (S ⨉_{𝑠} R) ↾_{𝑠} B$

Metamath Proof Explorer

Theorem dsmmval2

Proof