ringlsmss2

Description: The product with an ideal of a ring is a subset of that ideal. (Contributed by Thierry Arnoux, 2-Jun-2024)

	Ref	Expression
Hypotheses	ringlsmss.1	$⊢ B = {Base}_{R}$
	ringlsmss.2	$⊢ G = {mulGrp}_{R}$
	ringlsmss.3	$⊢ \underset{˙}{\times} = LSSum (G)$
	ringlsmss2.1	$⊢ φ \to R \in Ring$
	ringlsmss2.2	$⊢ φ \to E \subseteq B$
	ringlsmss2.3	$⊢ φ \to I \in LIdeal (R)$
Assertion	ringlsmss2	$⊢ φ \to E \underset{˙}{\times} I \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		ringlsmss2.1	$⊢ φ \to R \in Ring$
5		ringlsmss2.2	$⊢ φ \to E \subseteq B$
6		ringlsmss2.3	$⊢ φ \to I \in LIdeal (R)$
7		simpr	$⊢ ((((φ \land a \in (E \underset{˙}{\times} I)) \land e \in E) \land i \in I) \land a = e \cdot_{R} i) \to a = e \cdot_{R} i$
8	4	ad2antrr	$⊢ ((φ \land e \in E) \land i \in I) \to R \in Ring$
9	6	ad2antrr	$⊢ ((φ \land e \in E) \land i \in I) \to I \in LIdeal (R)$
10	5	sselda	$⊢ (φ \land e \in E) \to e \in B$
11	10	adantr	$⊢ ((φ \land e \in E) \land i \in I) \to e \in B$
12		simpr	$⊢ ((φ \land e \in E) \land i \in I) \to i \in I$
13		eqid	$⊢ LIdeal (R) = LIdeal (R)$
14		eqid	$⊢ \cdot_{R} = \cdot_{R}$
15	13 1 14	lidlmcl	$⊢ ((R \in Ring \land I \in LIdeal (R)) \land (e \in B \land i \in I)) \to e \cdot_{R} i \in I$
16	8 9 11 12 15	syl22anc	$⊢ ((φ \land e \in E) \land i \in I) \to e \cdot_{R} i \in I$
17	16	adantllr	$⊢ (((φ \land a \in (E \underset{˙}{\times} I)) \land e \in E) \land i \in I) \to e \cdot_{R} i \in I$
18	17	adantr	$⊢ ((((φ \land a \in (E \underset{˙}{\times} I)) \land e \in E) \land i \in I) \land a = e \cdot_{R} i) \to e \cdot_{R} i \in I$
19	7 18	eqeltrd	$⊢ ((((φ \land a \in (E \underset{˙}{\times} I)) \land e \in E) \land i \in I) \land a = e \cdot_{R} i) \to a \in I$
20	1 13	lidlss	$⊢ I \in LIdeal (R) \to I \subseteq B$
21	6 20	syl	$⊢ φ \to I \subseteq B$
22	1 14 2 3 5 21	elringlsm	$⊢ φ \to (a \in (E \underset{˙}{\times} I) \leftrightarrow \exists e \in E \exists i \in I a = e \cdot_{R} i)$
23	22	biimpa	$⊢ (φ \land a \in (E \underset{˙}{\times} I)) \to \exists e \in E \exists i \in I a = e \cdot_{R} i$
24	19 23	r19.29vva	$⊢ (φ \land a \in (E \underset{˙}{\times} I)) \to a \in I$
25	24	ex	$⊢ φ \to (a \in (E \underset{˙}{\times} I) \to a \in I)$
26	25	ssrdv	$⊢ φ \to E \underset{˙}{\times} I \subseteq I$

Metamath Proof Explorer

Theorem ringlsmss2

Proof