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=LIdealR
idlsrgmulrval.3 ˙=S
idlsrgmulrcl.1 φRRing
idlsrgmulrcl.2 φIB
idlsrgmulrcl.3 φJB
Assertion idlsrgmulrcl φI˙JB

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=LIdealR
3 idlsrgmulrval.3 ˙=S
4 idlsrgmulrcl.1 φRRing
5 idlsrgmulrcl.2 φIB
6 idlsrgmulrcl.3 φJB
7 eqid mulGrpR=mulGrpR
8 eqid LSSummulGrpR=LSSummulGrpR
9 1 2 3 7 8 4 5 6 idlsrgmulrval φI˙J=RSpanRILSSummulGrpRJ
10 eqid BaseR=BaseR
11 10 2 lidlss IBIBaseR
12 5 11 syl φIBaseR
13 10 2 lidlss JBJBaseR
14 6 13 syl φJBaseR
15 10 7 8 4 12 14 ringlsmss φILSSummulGrpRJBaseR
16 eqid RSpanR=RSpanR
17 16 10 2 rspcl RRingILSSummulGrpRJBaseRRSpanRILSSummulGrpRJB
18 4 15 17 syl2anc φRSpanRILSSummulGrpRJB
19 9 18 eqeltrd φI˙JB