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

Proof

Step Hyp Ref Expression
1 idlsrgmnd.1 ⊢ S = IDLsrg ⁡ R
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