Metamath Proof Explorer

Theorem idlsrgmnd

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

Ref Expression
Hypothesis idlsrgmnd.1 
|- S = ( IDLsrg ` R )
Assertion idlsrgmnd 
|- ( R e. Ring -> S e. Mnd )

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 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 eqid 
 |-  ( RSpan ` R ) = ( RSpan ` R )
8 simp1 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) /\ j e. ( LIdeal ` R ) ) -> R e. Ring )
9 simp2 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) /\ j e. ( LIdeal ` R ) ) -> i e. ( LIdeal ` R ) )
10 simp3 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) /\ j e. ( LIdeal ` R ) ) -> j e. ( LIdeal ` R ) )
11 6 4 7 8 9 10 lsmidl 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) /\ j e. ( LIdeal ` R ) ) -> ( i ( LSSum ` R ) j ) e. ( LIdeal ` R ) )
12 2 lidlsubg 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) ) -> i e. ( SubGrp ` R ) )
13 12 3ad2antr1 
 |-  ( ( R e. Ring /\ ( i e. ( LIdeal ` R ) /\ j e. ( LIdeal ` R ) /\ k e. ( LIdeal ` R ) ) ) -> i e. ( SubGrp ` R ) )
14 2 lidlsubg 
 |-  ( ( R e. Ring /\ j e. ( LIdeal ` R ) ) -> j e. ( SubGrp ` R ) )
15 14 3ad2antr2 
 |-  ( ( R e. Ring /\ ( i e. ( LIdeal ` R ) /\ j e. ( LIdeal ` R ) /\ k e. ( LIdeal ` R ) ) ) -> j e. ( SubGrp ` R ) )
16 2 lidlsubg 
 |-  ( ( R e. Ring /\ k e. ( LIdeal ` R ) ) -> k e. ( SubGrp ` R ) )
17 16 3ad2antr3 
 |-  ( ( R e. Ring /\ ( i e. ( LIdeal ` R ) /\ j e. ( LIdeal ` R ) /\ k e. ( LIdeal ` R ) ) ) -> k e. ( SubGrp ` R ) )
18 4 lsmass 
 |-  ( ( i e. ( SubGrp ` R ) /\ j e. ( SubGrp ` R ) /\ k e. ( SubGrp ` R ) ) -> ( ( i ( LSSum ` R ) j ) ( LSSum ` R ) k ) = ( i ( LSSum ` R ) ( j ( LSSum ` R ) k ) ) )
19 13 15 17 18 syl3anc 
 |-  ( ( R e. Ring /\ ( i e. ( LIdeal ` R ) /\ j e. ( LIdeal ` R ) /\ k e. ( LIdeal ` R ) ) ) -> ( ( i ( LSSum ` R ) j ) ( LSSum ` R ) k ) = ( i ( LSSum ` R ) ( j ( LSSum ` R ) k ) ) )
20 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
21 2 20 lidl0 
 |-  ( R e. Ring -> { ( 0g ` R ) } e. ( LIdeal ` R ) )
22 20 4 lsm02 
 |-  ( i e. ( SubGrp ` R ) -> ( { ( 0g ` R ) } ( LSSum ` R ) i ) = i )
23 12 22 syl 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) ) -> ( { ( 0g ` R ) } ( LSSum ` R ) i ) = i )
24 20 4 lsm01 
 |-  ( i e. ( SubGrp ` R ) -> ( i ( LSSum ` R ) { ( 0g ` R ) } ) = i )
25 12 24 syl 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) ) -> ( i ( LSSum ` R ) { ( 0g ` R ) } ) = i )
26 3 5 11 19 21 23 25 ismndd 
 |-  ( R e. Ring -> S e. Mnd )