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 ⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
Assertion idlsrgmnd ( 𝑅 ∈ Ring → 𝑆 ∈ Mnd )

Proof

Step Hyp Ref Expression
1 idlsrgmnd.1 ⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
2 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
3 1 2 idlsrgbas ⊢ ( 𝑅 ∈ Ring → ( LIdeal ‘ 𝑅 ) = ( Base ‘ 𝑆 ) )
4 eqid ⊢ ( LSSum ‘ 𝑅 ) = ( LSSum ‘ 𝑅 )
5 1 4 idlsrgplusg ⊢ ( 𝑅 ∈ Ring → ( LSSum ‘ 𝑅 ) = ( +g ‘ 𝑆 ) )
6 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 eqid ⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
8 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
9 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
10 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑗 ∈ ( LIdeal ‘ 𝑅 ) )
11 6 4 7 8 9 10 lsmidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑖 ( LSSum ‘ 𝑅 ) 𝑗 ) ∈ ( LIdeal ‘ 𝑅 ) )
12 2 lidlsubg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑖 ∈ ( SubGrp ‘ 𝑅 ) )
13 12 3ad2antr1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ) → 𝑖 ∈ ( SubGrp ‘ 𝑅 ) )
14 2 lidlsubg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑗 ∈ ( SubGrp ‘ 𝑅 ) )
15 14 3ad2antr2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ) → 𝑗 ∈ ( SubGrp ‘ 𝑅 ) )
16 2 lidlsubg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑘 ∈ ( SubGrp ‘ 𝑅 ) )
17 16 3ad2antr3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ) → 𝑘 ∈ ( SubGrp ‘ 𝑅 ) )
18 4 lsmass ⊢ ( ( 𝑖 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑗 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑘 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ( 𝑖 ( LSSum ‘ 𝑅 ) 𝑗 ) ( LSSum ‘ 𝑅 ) 𝑘 ) = ( 𝑖 ( LSSum ‘ 𝑅 ) ( 𝑗 ( LSSum ‘ 𝑅 ) 𝑘 ) ) )
19 13 15 17 18 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ) → ( ( 𝑖 ( LSSum ‘ 𝑅 ) 𝑗 ) ( LSSum ‘ 𝑅 ) 𝑘 ) = ( 𝑖 ( LSSum ‘ 𝑅 ) ( 𝑗 ( LSSum ‘ 𝑅 ) 𝑘 ) ) )
20 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
21 2 20 lidl0 ⊢ ( 𝑅 ∈ Ring → { ( 0g ‘ 𝑅 ) } ∈ ( LIdeal ‘ 𝑅 ) )
22 20 4 lsm02 ⊢ ( 𝑖 ∈ ( SubGrp ‘ 𝑅 ) → ( { ( 0g ‘ 𝑅 ) } ( LSSum ‘ 𝑅 ) 𝑖 ) = 𝑖 )
23 12 22 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → ( { ( 0g ‘ 𝑅 ) } ( LSSum ‘ 𝑅 ) 𝑖 ) = 𝑖 )
24 20 4 lsm01 ⊢ ( 𝑖 ∈ ( SubGrp ‘ 𝑅 ) → ( 𝑖 ( LSSum ‘ 𝑅 ) { ( 0g ‘ 𝑅 ) } ) = 𝑖 )
25 12 24 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑖 ( LSSum ‘ 𝑅 ) { ( 0g ‘ 𝑅 ) } ) = 𝑖 )
26 3 5 11 19 21 23 25 ismndd ⊢ ( 𝑅 ∈ Ring → 𝑆 ∈ Mnd )