dsmmbas2

Description: Base set of the direct sum module using the fndmin abbreviation. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Hypotheses	dsmmbas2.p	$⊢ P = S ⨉_{𝑠} R$
	dsmmbas2.b	$⊢ B = \{f \in {Base}_{P} \| dom (f ∖ (0_{𝑔} \circ R)) \in Fin\}$
Assertion	dsmmbas2	$⊢ (R Fn I \land I \in V) \to B = {Base}_{(S \oplus_{m} R)}$

Proof

Step	Hyp	Ref	Expression
1		dsmmbas2.p	$⊢ P = S ⨉_{𝑠} R$
2		dsmmbas2.b	$⊢ B = \{f \in {Base}_{P} \| dom (f ∖ (0_{𝑔} \circ R)) \in Fin\}$
3	1	fveq2i	$⊢ {Base}_{P} = {Base}_{(S ⨉_{𝑠} R)}$
4	3	rabeqi	$⊢ \{f \in {Base}_{P} \| dom (f ∖ (0_{𝑔} \circ R)) \in Fin\} = \{f \in {Base}_{(S ⨉_{𝑠} R)} \| dom (f ∖ (0_{𝑔} \circ R)) \in Fin\}$
5		simpll	$⊢ ((R Fn I \land I \in V) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to R Fn I$
6		fvco2	$⊢ (R Fn I \land x \in I) \to (0_{𝑔} \circ R) (x) = 0_{R (x)}$
7	5 6	sylan	$⊢ (((R Fn I \land I \in V) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \land x \in I) \to (0_{𝑔} \circ R) (x) = 0_{R (x)}$
8	7	neeq2d	$⊢ (((R Fn I \land I \in V) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \land x \in I) \to (f (x) \neq (0_{𝑔} \circ R) (x) \leftrightarrow f (x) \neq 0_{R (x)})$
9	8	rabbidva	$⊢ ((R Fn I \land I \in V) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to \{x \in I \| f (x) \neq (0_{𝑔} \circ R) (x)\} = \{x \in I \| f (x) \neq 0_{R (x)}\}$
10		eqid	$⊢ S ⨉_{𝑠} R = S ⨉_{𝑠} R$
11		eqid	$⊢ {Base}_{(S ⨉_{𝑠} R)} = {Base}_{(S ⨉_{𝑠} R)}$
12		reldmprds	$⊢ Rel dom ⨉_{𝑠}$
13	10 11 12	strov2rcl	$⊢ f \in {Base}_{(S ⨉_{𝑠} R)} \to S \in V$
14	13	adantl	$⊢ ((R Fn I \land I \in V) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to S \in V$
15		simplr	$⊢ ((R Fn I \land I \in V) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to I \in V$
16		simpr	$⊢ ((R Fn I \land I \in V) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to f \in {Base}_{(S ⨉_{𝑠} R)}$
17	10 11 14 15 5 16	prdsbasfn	$⊢ ((R Fn I \land I \in V) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to f Fn I$
18		fn0g	$⊢ 0_{𝑔} Fn V$
19		dffn2	$⊢ 0_{𝑔} Fn V \leftrightarrow 0_{𝑔} : V ⟶ V$
20	18 19	mpbi	$⊢ 0_{𝑔} : V ⟶ V$
21		dffn2	$⊢ R Fn I \leftrightarrow R : I ⟶ V$
22	21	biimpi	$⊢ R Fn I \to R : I ⟶ V$
23		fco	$⊢ (0_{𝑔} : V ⟶ V \land R : I ⟶ V) \to (0_{𝑔} \circ R) : I ⟶ V$
24	20 22 23	sylancr	$⊢ R Fn I \to (0_{𝑔} \circ R) : I ⟶ V$
25	24	ffnd	$⊢ R Fn I \to (0_{𝑔} \circ R) Fn I$
26	5 25	syl	$⊢ ((R Fn I \land I \in V) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to (0_{𝑔} \circ R) Fn I$
27		fndmdif	$⊢ (f Fn I \land (0_{𝑔} \circ R) Fn I) \to dom (f ∖ (0_{𝑔} \circ R)) = \{x \in I \| f (x) \neq (0_{𝑔} \circ R) (x)\}$
28	17 26 27	syl2anc	$⊢ ((R Fn I \land I \in V) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to dom (f ∖ (0_{𝑔} \circ R)) = \{x \in I \| f (x) \neq (0_{𝑔} \circ R) (x)\}$
29		fndm	$⊢ R Fn I \to dom R = I$
30	29	rabeqdv	$⊢ R Fn I \to \{x \in dom R \| f (x) \neq 0_{R (x)}\} = \{x \in I \| f (x) \neq 0_{R (x)}\}$
31	5 30	syl	$⊢ ((R Fn I \land I \in V) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to \{x \in dom R \| f (x) \neq 0_{R (x)}\} = \{x \in I \| f (x) \neq 0_{R (x)}\}$
32	9 28 31	3eqtr4d	$⊢ ((R Fn I \land I \in V) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to dom (f ∖ (0_{𝑔} \circ R)) = \{x \in dom R \| f (x) \neq 0_{R (x)}\}$
33	32	eleq1d	$⊢ ((R Fn I \land I \in V) \land f \in {Base}_{(S ⨉_{𝑠} R)}) \to (dom (f ∖ (0_{𝑔} \circ R)) \in Fin \leftrightarrow \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin)$
34	33	rabbidva	$⊢ (R Fn I \land I \in V) \to \{f \in {Base}_{(S ⨉_{𝑠} R)} \| dom (f ∖ (0_{𝑔} \circ R)) \in Fin\} = \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\}$
35	4 34	syl5eq	$⊢ (R Fn I \land I \in V) \to \{f \in {Base}_{P} \| dom (f ∖ (0_{𝑔} \circ R)) \in Fin\} = \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\}$
36		fnex	$⊢ (R Fn I \land I \in V) \to R \in V$
37		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\}$
38	37	dsmmbase	$⊢ R \in V \to \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\} = {Base}_{(S \oplus_{m} R)}$
39	36 38	syl	$⊢ (R Fn I \land I \in V) \to \{f \in {Base}_{(S ⨉_{𝑠} R)} \| \{x \in dom R \| f (x) \neq 0_{R (x)}\} \in Fin\} = {Base}_{(S \oplus_{m} R)}$
40	35 39	eqtrd	$⊢ (R Fn I \land I \in V) \to \{f \in {Base}_{P} \| dom (f ∖ (0_{𝑔} \circ R)) \in Fin\} = {Base}_{(S \oplus_{m} R)}$
41	2 40	syl5eq	$⊢ (R Fn I \land I \in V) \to B = {Base}_{(S \oplus_{m} R)}$

Metamath Proof Explorer

Theorem dsmmbas2

Proof