dsmmfi

Description: For finite products, the direct sum is just the module product. See also the observation in Lang p. 129. (Contributed by Stefan O'Rear, 1-Feb-2015)

		Ref	Expression
	Assertion	dsmmfi	$⊢ (R Fn I \land I \in Fin) \to S \oplus_{m} R = S ⨉_{𝑠} R$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{(S \oplus_{m} R)} = {Base}_{(S \oplus_{m} R)}$
2	1	dsmmval2	$⊢ S \oplus_{m} R = (S ⨉_{𝑠} R) ↾_{𝑠} {Base}_{(S \oplus_{m} R)}$
3		eqid	$⊢ S ⨉_{𝑠} R = S ⨉_{𝑠} R$
4		eqid	$⊢ {Base}_{(S ⨉_{𝑠} R)} = {Base}_{(S ⨉_{𝑠} R)}$
5		noel	$⊢ \neg f \in \emptyset$
6		reldmprds	$⊢ Rel dom ⨉_{𝑠}$
7	6	ovprc1	$⊢ \neg S \in V \to S ⨉_{𝑠} R = \emptyset$
8	7	fveq2d	$⊢ \neg S \in V \to {Base}_{(S ⨉_{𝑠} R)} = {Base}_{\emptyset}$
9		base0	$⊢ \emptyset = {Base}_{\emptyset}$
10	8 9	eqtr4di	$⊢ \neg S \in V \to {Base}_{(S ⨉_{𝑠} R)} = \emptyset$
11	10	eleq2d	$⊢ \neg S \in V \to (f \in {Base}_{(S ⨉_{𝑠} R)} \leftrightarrow f \in \emptyset)$
12	5 11	mtbiri	$⊢ \neg S \in V \to \neg f \in {Base}_{(S ⨉_{𝑠} R)}$
13	12	con4i	$⊢ f \in {Base}_{(S ⨉_{𝑠} R)} \to S \in V$
14	13	adantl	$⊢ ((R Fn I \land I \in Fin) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to S \in V$
15		simplr	$⊢ ((R Fn I \land I \in Fin) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to I \in Fin$
16		simpll	$⊢ ((R Fn I \land I \in Fin) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to R Fn I$
17		simpr	$⊢ ((R Fn I \land I \in Fin) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to f \in {Base}_{(S ⨉_{𝑠} R)}$
18	3 4 14 15 16 17	prdsbasfn	$⊢ ((R Fn I \land I \in Fin) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to f Fn I$
19	18	fndmd	$⊢ ((R Fn I \land I \in Fin) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to dom f = I$
20	19 15	eqeltrd	$⊢ ((R Fn I \land I \in Fin) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to dom f \in Fin$
21		difss	$⊢ f ∖ (0_{𝑔} \circ R) \subseteq f$
22		dmss	$⊢ f ∖ (0_{𝑔} \circ R) \subseteq f \to dom (f ∖ (0_{𝑔} \circ R)) \subseteq dom f$
23	21 22	ax-mp	$⊢ dom (f ∖ (0_{𝑔} \circ R)) \subseteq dom f$
24		ssfi	$⊢ (dom f \in Fin \land dom (f ∖ (0_{𝑔} \circ R)) \subseteq dom f) \to dom (f ∖ (0_{𝑔} \circ R)) \in Fin$
25	20 23 24	sylancl	$⊢ ((R Fn I \land I \in Fin) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to dom (f ∖ (0_{𝑔} \circ R)) \in Fin$
26	25	ralrimiva	$⊢ (R Fn I \land I \in Fin) \to \forall f \in {Base}_{(S ⨉_{𝑠} R)} dom (f ∖ (0_{𝑔} \circ R)) \in Fin$
27		rabid2	$⊢ {Base}_{(S ⨉_{𝑠} R)} = \{f \in {Base}_{(S ⨉_{𝑠} R)} \| dom (f ∖ (0_{𝑔} \circ R)) \in Fin\} \leftrightarrow \forall f \in {Base}_{(S ⨉_{𝑠} R)} dom (f ∖ (0_{𝑔} \circ R)) \in Fin$
28	26 27	sylibr	$⊢ (R Fn I \land I \in Fin) \to {Base}_{(S ⨉_{𝑠} R)} = \{f \in {Base}_{(S ⨉_{𝑠} R)} \| dom (f ∖ (0_{𝑔} \circ R)) \in Fin\}$
29		eqid	$⊢ \{f \in {Base}_{(S ⨉_{𝑠} R)} \| dom (f ∖ (0_{𝑔} \circ R)) \in Fin\} = \{f \in {Base}_{(S ⨉_{𝑠} R)} \| dom (f ∖ (0_{𝑔} \circ R)) \in Fin\}$
30	3 29	dsmmbas2	$⊢ (R Fn I \land I \in Fin) \to \{f \in {Base}_{(S ⨉_{𝑠} R)} \| dom (f ∖ (0_{𝑔} \circ R)) \in Fin\} = {Base}_{(S \oplus_{m} R)}$
31	28 30	eqtr2d	$⊢ (R Fn I \land I \in Fin) \to {Base}_{(S \oplus_{m} R)} = {Base}_{(S ⨉_{𝑠} R)}$
32	31	oveq2d	$⊢ (R Fn I \land I \in Fin) \to (S ⨉_{𝑠} R) ↾_{𝑠} {Base}_{(S \oplus_{m} R)} = (S ⨉_{𝑠} R) ↾_{𝑠} {Base}_{(S ⨉_{𝑠} R)}$
33		ovex	$⊢ S ⨉_{𝑠} R \in V$
34	4	ressid	$⊢ S ⨉_{𝑠} R \in V \to (S ⨉_{𝑠} R) ↾_{𝑠} {Base}_{(S ⨉_{𝑠} R)} = S ⨉_{𝑠} R$
35	33 34	ax-mp	$⊢ (S ⨉_{𝑠} R) ↾_{𝑠} {Base}_{(S ⨉_{𝑠} R)} = S ⨉_{𝑠} R$
36	32 35	eqtrdi	$⊢ (R Fn I \land I \in Fin) \to (S ⨉_{𝑠} R) ↾_{𝑠} {Base}_{(S \oplus_{m} R)} = S ⨉_{𝑠} R$
37	2 36	syl5eq	$⊢ (R Fn I \land I \in Fin) \to S \oplus_{m} R = S ⨉_{𝑠} R$

Metamath Proof Explorer

Theorem dsmmfi

Proof