dsmmelbas

Description: Membership in the finitely supported hull of a structure product in terms of the index set. (Contributed by Stefan O'Rear, 11-Jan-2015)

	Ref	Expression
Hypotheses	dsmmelbas.p	$⊢ P = S ⨉_{𝑠} R$
	dsmmelbas.c	$⊢ C = S \oplus_{m} R$
	dsmmelbas.b	$⊢ B = {Base}_{P}$
	dsmmelbas.h	$⊢ H = {Base}_{C}$
	dsmmelbas.i	$⊢ φ \to I \in V$
	dsmmelbas.r	$⊢ φ \to R Fn I$
Assertion	dsmmelbas	$⊢ φ \to (X \in H \leftrightarrow (X \in B \land \{a \in I \| X (a) \neq 0_{R (a)}\} \in Fin))$

Proof

Step	Hyp	Ref	Expression
1		dsmmelbas.p	$⊢ P = S ⨉_{𝑠} R$
2		dsmmelbas.c	$⊢ C = S \oplus_{m} R$
3		dsmmelbas.b	$⊢ B = {Base}_{P}$
4		dsmmelbas.h	$⊢ H = {Base}_{C}$
5		dsmmelbas.i	$⊢ φ \to I \in V$
6		dsmmelbas.r	$⊢ φ \to R Fn I$
7	2	fveq2i	$⊢ {Base}_{C} = {Base}_{(S \oplus_{m} R)}$
8	4 7	eqtri	$⊢ H = {Base}_{(S \oplus_{m} R)}$
9		fnex	$⊢ (R Fn I \land I \in V) \to R \in V$
10	6 5 9	syl2anc	$⊢ φ \to R \in V$
11		eqid	$⊢ \{b \in {Base}_{(S ⨉_{𝑠} R)} \| \{a \in dom R \| b (a) \neq 0_{R (a)}\} \in Fin\} = \{b \in {Base}_{(S ⨉_{𝑠} R)} \| \{a \in dom R \| b (a) \neq 0_{R (a)}\} \in Fin\}$
12	11	dsmmbase	$⊢ R \in V \to \{b \in {Base}_{(S ⨉_{𝑠} R)} \| \{a \in dom R \| b (a) \neq 0_{R (a)}\} \in Fin\} = {Base}_{(S \oplus_{m} R)}$
13	10 12	syl	$⊢ φ \to \{b \in {Base}_{(S ⨉_{𝑠} R)} \| \{a \in dom R \| b (a) \neq 0_{R (a)}\} \in Fin\} = {Base}_{(S \oplus_{m} R)}$
14	8 13	eqtr4id	$⊢ φ \to H = \{b \in {Base}_{(S ⨉_{𝑠} R)} \| \{a \in dom R \| b (a) \neq 0_{R (a)}\} \in Fin\}$
15	14	eleq2d	$⊢ φ \to (X \in H \leftrightarrow X \in \{b \in {Base}_{(S ⨉_{𝑠} R)} \| \{a \in dom R \| b (a) \neq 0_{R (a)}\} \in Fin\})$
16		fveq1	$⊢ b = X \to b (a) = X (a)$
17	16	neeq1d	$⊢ b = X \to (b (a) \neq 0_{R (a)} \leftrightarrow X (a) \neq 0_{R (a)})$
18	17	rabbidv	$⊢ b = X \to \{a \in dom R \| b (a) \neq 0_{R (a)}\} = \{a \in dom R \| X (a) \neq 0_{R (a)}\}$
19	18	eleq1d	$⊢ b = X \to (\{a \in dom R \| b (a) \neq 0_{R (a)}\} \in Fin \leftrightarrow \{a \in dom R \| X (a) \neq 0_{R (a)}\} \in Fin)$
20	19	elrab	$⊢ X \in \{b \in {Base}_{(S ⨉_{𝑠} R)} \| \{a \in dom R \| b (a) \neq 0_{R (a)}\} \in Fin\} \leftrightarrow (X \in {Base}_{(S ⨉_{𝑠} R)} \land \{a \in dom R \| X (a) \neq 0_{R (a)}\} \in Fin)$
21	1	fveq2i	$⊢ {Base}_{P} = {Base}_{(S ⨉_{𝑠} R)}$
22	3 21	eqtr2i	$⊢ {Base}_{(S ⨉_{𝑠} R)} = B$
23	22	eleq2i	$⊢ X \in {Base}_{(S ⨉_{𝑠} R)} \leftrightarrow X \in B$
24	23	a1i	$⊢ φ \to (X \in {Base}_{(S ⨉_{𝑠} R)} \leftrightarrow X \in B)$
25		fndm	$⊢ R Fn I \to dom R = I$
26		rabeq	$⊢ dom R = I \to \{a \in dom R \| X (a) \neq 0_{R (a)}\} = \{a \in I \| X (a) \neq 0_{R (a)}\}$
27	6 25 26	3syl	$⊢ φ \to \{a \in dom R \| X (a) \neq 0_{R (a)}\} = \{a \in I \| X (a) \neq 0_{R (a)}\}$
28	27	eleq1d	$⊢ φ \to (\{a \in dom R \| X (a) \neq 0_{R (a)}\} \in Fin \leftrightarrow \{a \in I \| X (a) \neq 0_{R (a)}\} \in Fin)$
29	24 28	anbi12d	$⊢ φ \to ((X \in {Base}_{(S ⨉_{𝑠} R)} \land \{a \in dom R \| X (a) \neq 0_{R (a)}\} \in Fin) \leftrightarrow (X \in B \land \{a \in I \| X (a) \neq 0_{R (a)}\} \in Fin))$
30	20 29	bitrid	$⊢ φ \to (X \in \{b \in {Base}_{(S ⨉_{𝑠} R)} \| \{a \in dom R \| b (a) \neq 0_{R (a)}\} \in Fin\} \leftrightarrow (X \in B \land \{a \in I \| X (a) \neq 0_{R (a)}\} \in Fin))$
31	15 30	bitrd	$⊢ φ \to (X \in H \leftrightarrow (X \in B \land \{a \in I \| X (a) \neq 0_{R (a)}\} \in Fin))$

Metamath Proof Explorer

Theorem dsmmelbas

Proof