Metamath Proof Explorer


Theorem idlsrgmulrcl

Description: Ideals of a ring R are closed under multiplication. (Contributed by Thierry Arnoux, 1-Jun-2024)

Ref Expression
Hypotheses idlsrgmulrval.1 No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
idlsrgmulrval.2 B = LIdeal R
idlsrgmulrval.3 ˙ = S
idlsrgmulrcl.1 φ R Ring
idlsrgmulrcl.2 φ I B
idlsrgmulrcl.3 φ J B
Assertion idlsrgmulrcl φ I ˙ J B

Proof

Step Hyp Ref Expression
1 idlsrgmulrval.1 Could not format S = ( IDLsrg ` R ) : No typesetting found for |- S = ( IDLsrg ` R ) with typecode |-
2 idlsrgmulrval.2 B = LIdeal R
3 idlsrgmulrval.3 ˙ = S
4 idlsrgmulrcl.1 φ R Ring
5 idlsrgmulrcl.2 φ I B
6 idlsrgmulrcl.3 φ J B
7 eqid mulGrp R = mulGrp R
8 eqid LSSum mulGrp R = LSSum mulGrp R
9 1 2 3 7 8 4 5 6 idlsrgmulrval φ I ˙ J = RSpan R I LSSum mulGrp R J
10 eqid Base R = Base R
11 10 2 lidlss I B I Base R
12 5 11 syl φ I Base R
13 10 2 lidlss J B J Base R
14 6 13 syl φ J Base R
15 10 7 8 4 12 14 ringlsmss φ I LSSum mulGrp R J Base R
16 eqid RSpan R = RSpan R
17 16 10 2 rspcl R Ring I LSSum mulGrp R J Base R RSpan R I LSSum mulGrp R J B
18 4 15 17 syl2anc φ RSpan R I LSSum mulGrp R J B
19 9 18 eqeltrd φ I ˙ J B