Metamath Proof Explorer

Theorem 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 ∈ Ring → S ∈ CMnd

Proof

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 ∈ Ring → LIdeal ⁡ R = Base S
4 eqid ⊢ LSSum ⁡ R = LSSum ⁡ R
5 1 4 idlsrgplusg ⊢ R ∈ Ring → LSSum ⁡ R = + S
6 1 idlsrgmnd ⊢ R ∈ Ring → S ∈ Mnd
7 ringabl ⊢ R ∈ Ring → R ∈ Abel
8 7 3ad2ant1 ⊢ R ∈ Ring ∧ i ∈ LIdeal ⁡ R ∧ j ∈ LIdeal ⁡ R → R ∈ Abel
9 2 lidlsubg ⊢ R ∈ Ring ∧ i ∈ LIdeal ⁡ R → i ∈ SubGrp ⁡ R
10 9 3adant3 ⊢ R ∈ Ring ∧ i ∈ LIdeal ⁡ R ∧ j ∈ LIdeal ⁡ R → i ∈ SubGrp ⁡ R
11 2 lidlsubg ⊢ R ∈ Ring ∧ j ∈ LIdeal ⁡ R → j ∈ SubGrp ⁡ R
12 11 3adant2 ⊢ R ∈ Ring ∧ i ∈ LIdeal ⁡ R ∧ j ∈ LIdeal ⁡ R → j ∈ SubGrp ⁡ R
13 4 lsmcom ⊢ R ∈ Abel ∧ i ∈ SubGrp ⁡ R ∧ j ∈ SubGrp ⁡ R → i LSSum ⁡ R j = j LSSum ⁡ R i
14 8 10 12 13 syl3anc ⊢ R ∈ Ring ∧ i ∈ LIdeal ⁡ R ∧ j ∈ LIdeal ⁡ R → i LSSum ⁡ R j = j LSSum ⁡ R i
15 3 5 6 14 iscmnd ⊢ R ∈ Ring → S ∈ CMnd