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 No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
Assertion idlsrgmnd R Ring S Mnd

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