Theorem idlsrgcmnd

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

	Ref	Expression
Hypothesis	idlsrgmnd.1	⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
Assertion	idlsrgcmnd	⊢ ( 𝑅 ∈ Ring → 𝑆 ∈ CMnd )

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	1	idlsrgmnd	⊢ ( 𝑅 ∈ Ring → 𝑆 ∈ Mnd )
7		ringabl	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
8	7	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑅 ∈ Abel )
9	2	lidlsubg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑖 ∈ ( SubGrp ‘ 𝑅 ) )
10	9	3adant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑖 ∈ ( SubGrp ‘ 𝑅 ) )
11	2	lidlsubg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑗 ∈ ( SubGrp ‘ 𝑅 ) )
12	11	3adant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑗 ∈ ( SubGrp ‘ 𝑅 ) )
13	4	lsmcom	⊢ ( ( 𝑅 ∈ Abel ∧ 𝑖 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑗 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝑖 ( LSSum ‘ 𝑅 ) 𝑗 ) = ( 𝑗 ( LSSum ‘ 𝑅 ) 𝑖 ) )
14	8 10 12 13	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑖 ( LSSum ‘ 𝑅 ) 𝑗 ) = ( 𝑗 ( LSSum ‘ 𝑅 ) 𝑖 ) )
15	3 5 6 14	iscmnd	⊢ ( 𝑅 ∈ Ring → 𝑆 ∈ CMnd )