ringlsmss1

Description: The product of an ideal I of a commutative ring R with some set E is a subset of the ideal. (Contributed by Thierry Arnoux, 8-Jun-2024)

	Ref	Expression
Hypotheses	ringlsmss.1	$⊢ B = {Base}_{R}$
	ringlsmss.2	$⊢ G = {mulGrp}_{R}$
	ringlsmss.3	$⊢ \underset{˙}{\times} = LSSum (G)$
	ringlsmss1.1	$⊢ φ \to R \in CRing$
	ringlsmss1.2	$⊢ φ \to E \subseteq B$
	ringlsmss1.3	$⊢ φ \to I \in LIdeal (R)$
Assertion	ringlsmss1	$⊢ φ \to I \underset{˙}{\times} E \subseteq I$

Proof

Step	Hyp	Ref	Expression
1		ringlsmss.1	$⊢ B = {Base}_{R}$
2		ringlsmss.2	$⊢ G = {mulGrp}_{R}$
3		ringlsmss.3	$⊢ \underset{˙}{\times} = LSSum (G)$
4		ringlsmss1.1	$⊢ φ \to R \in CRing$
5		ringlsmss1.2	$⊢ φ \to E \subseteq B$
6		ringlsmss1.3	$⊢ φ \to I \in LIdeal (R)$
7		simpr	$⊢ ((((φ \land a \in (I \underset{˙}{\times} E)) \land i \in I) \land e \in E) \land a = i \cdot_{R} e) \to a = i \cdot_{R} e$
8	4	ad2antrr	$⊢ ((φ \land i \in I) \land e \in E) \to R \in CRing$
9	5	sselda	$⊢ (φ \land e \in E) \to e \in B$
10	9	adantlr	$⊢ ((φ \land i \in I) \land e \in E) \to e \in B$
11		eqid	$⊢ LIdeal (R) = LIdeal (R)$
12	1 11	lidlss	$⊢ I \in LIdeal (R) \to I \subseteq B$
13	6 12	syl	$⊢ φ \to I \subseteq B$
14	13	sselda	$⊢ (φ \land i \in I) \to i \in B$
15	14	adantr	$⊢ ((φ \land i \in I) \land e \in E) \to i \in B$
16		eqid	$⊢ \cdot_{R} = \cdot_{R}$
17	1 16	crngcom	$⊢ (R \in CRing \land e \in B \land i \in B) \to e \cdot_{R} i = i \cdot_{R} e$
18	8 10 15 17	syl3anc	$⊢ ((φ \land i \in I) \land e \in E) \to e \cdot_{R} i = i \cdot_{R} e$
19		crngring	$⊢ R \in CRing \to R \in Ring$
20	4 19	syl	$⊢ φ \to R \in Ring$
21	20	ad2antrr	$⊢ ((φ \land i \in I) \land e \in E) \to R \in Ring$
22	6	ad2antrr	$⊢ ((φ \land i \in I) \land e \in E) \to I \in LIdeal (R)$
23		simplr	$⊢ ((φ \land i \in I) \land e \in E) \to i \in I$
24	11 1 16	lidlmcl	$⊢ ((R \in Ring \land I \in LIdeal (R)) \land (e \in B \land i \in I)) \to e \cdot_{R} i \in I$
25	21 22 10 23 24	syl22anc	$⊢ ((φ \land i \in I) \land e \in E) \to e \cdot_{R} i \in I$
26	18 25	eqeltrrd	$⊢ ((φ \land i \in I) \land e \in E) \to i \cdot_{R} e \in I$
27	26	adantllr	$⊢ (((φ \land a \in (I \underset{˙}{\times} E)) \land i \in I) \land e \in E) \to i \cdot_{R} e \in I$
28	27	adantr	$⊢ ((((φ \land a \in (I \underset{˙}{\times} E)) \land i \in I) \land e \in E) \land a = i \cdot_{R} e) \to i \cdot_{R} e \in I$
29	7 28	eqeltrd	$⊢ ((((φ \land a \in (I \underset{˙}{\times} E)) \land i \in I) \land e \in E) \land a = i \cdot_{R} e) \to a \in I$
30	1 16 2 3 13 5	elmgplsm	$⊢ φ \to (a \in (I \underset{˙}{\times} E) \leftrightarrow \exists i \in I \exists e \in E a = i \cdot_{R} e)$
31	30	biimpa	$⊢ (φ \land a \in (I \underset{˙}{\times} E)) \to \exists i \in I \exists e \in E a = i \cdot_{R} e$
32	29 31	r19.29vva	$⊢ (φ \land a \in (I \underset{˙}{\times} E)) \to a \in I$
33	32	ex	$⊢ φ \to (a \in (I \underset{˙}{\times} E) \to a \in I)$
34	33	ssrdv	$⊢ φ \to I \underset{˙}{\times} E \subseteq I$

Metamath Proof Explorer

Theorem ringlsmss1

Proof