idlsrgcmnd

Description: The ideals of a ring form a commutative monoid. (Contributed by Thierry Arnoux, 1-Jun-2024)

		Ref	Expression
	Hypothesis	idlsrgmnd.1	No typesetting found for \|- S = ( IDLsrg ` R ) with typecode \|-
	Assertion	idlsrgcmnd	$⊢ R \in Ring \to S \in CMnd$

Step	Hyp	Ref	Expression
1		idlsrgmnd.1	Could not format S = ( IDLsrg ` R ) : No typesetting found for \|- S = ( IDLsrg ` R ) with typecode \|-
2		eqid	$⊢ LIdeal (R) = LIdeal (R)$
3	1 2	idlsrgbas	$⊢ R \in Ring \to LIdeal (R) = {Base}_{S}$
4		eqid	$⊢ LSSum (R) = LSSum (R)$
5	1 4	idlsrgplusg	$⊢ R \in Ring \to LSSum (R) = +_{S}$
6	1	idlsrgmnd	$⊢ R \in Ring \to S \in Mnd$
7		ringabl	$⊢ R \in Ring \to R \in Abel$
8	7	3ad2ant1	$⊢ (R \in Ring \land i \in LIdeal (R) \land j \in LIdeal (R)) \to R \in Abel$
9	2	lidlsubg	$⊢ (R \in Ring \land i \in LIdeal (R)) \to i \in SubGrp (R)$
10	9	3adant3	$⊢ (R \in Ring \land i \in LIdeal (R) \land j \in LIdeal (R)) \to i \in SubGrp (R)$
11	2	lidlsubg	$⊢ (R \in Ring \land j \in LIdeal (R)) \to j \in SubGrp (R)$
12	11	3adant2	$⊢ (R \in Ring \land i \in LIdeal (R) \land j \in LIdeal (R)) \to j \in SubGrp (R)$
13	4	lsmcom	$⊢ (R \in Abel \land i \in SubGrp (R) \land j \in SubGrp (R)) \to i LSSum (R) j = j LSSum (R) i$
14	8 10 12 13	syl3anc	$⊢ (R \in Ring \land i \in LIdeal (R) \land j \in LIdeal (R)) \to i LSSum (R) j = j LSSum (R) i$
15	3 5 6 14	iscmnd	$⊢ R \in Ring \to S \in CMnd$

Metamath Proof Explorer