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 
|- S = ( IDLsrg ` R )
Assertion idlsrgcmnd 
|- ( R e. Ring -> S e. CMnd )

Proof

Step Hyp Ref Expression
1 idlsrgmnd.1 
 |-  S = ( IDLsrg ` R )
2 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
3 1 2 idlsrgbas 
 |-  ( R e. Ring -> ( LIdeal ` R ) = ( Base ` S ) )
4 eqid 
 |-  ( LSSum ` R ) = ( LSSum ` R )
5 1 4 idlsrgplusg 
 |-  ( R e. Ring -> ( LSSum ` R ) = ( +g ` S ) )
6 1 idlsrgmnd 
 |-  ( R e. Ring -> S e. Mnd )
7 ringabl 
 |-  ( R e. Ring -> R e. Abel )
8 7 3ad2ant1 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) /\ j e. ( LIdeal ` R ) ) -> R e. Abel )
9 2 lidlsubg 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) ) -> i e. ( SubGrp ` R ) )
10 9 3adant3 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) /\ j e. ( LIdeal ` R ) ) -> i e. ( SubGrp ` R ) )
11 2 lidlsubg 
 |-  ( ( R e. Ring /\ j e. ( LIdeal ` R ) ) -> j e. ( SubGrp ` R ) )
12 11 3adant2 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) /\ j e. ( LIdeal ` R ) ) -> j e. ( SubGrp ` R ) )
13 4 lsmcom 
 |-  ( ( R e. Abel /\ i e. ( SubGrp ` R ) /\ j e. ( SubGrp ` R ) ) -> ( i ( LSSum ` R ) j ) = ( j ( LSSum ` R ) i ) )
14 8 10 12 13 syl3anc 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) /\ j e. ( LIdeal ` R ) ) -> ( i ( LSSum ` R ) j ) = ( j ( LSSum ` R ) i ) )
15 3 5 6 14 iscmnd 
 |-  ( R e. Ring -> S e. CMnd )