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 | |
||
idlsrgmulrval.3 | |
||
idlsrgmulrcl.1 | |
||
idlsrgmulrcl.2 | |
||
idlsrgmulrcl.3 | |
||
Assertion | idlsrgmulrcl | |
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 | |
|
3 | idlsrgmulrval.3 | |
|
4 | idlsrgmulrcl.1 | |
|
5 | idlsrgmulrcl.2 | |
|
6 | idlsrgmulrcl.3 | |
|
7 | eqid | |
|
8 | eqid | |
|
9 | 1 2 3 7 8 4 5 6 | idlsrgmulrval | |
10 | eqid | |
|
11 | 10 2 | lidlss | |
12 | 5 11 | syl | |
13 | 10 2 | lidlss | |
14 | 6 13 | syl | |
15 | 10 7 8 4 12 14 | ringlsmss | |
16 | eqid | |
|
17 | 16 10 2 | rspcl | |
18 | 4 15 17 | syl2anc | |
19 | 9 18 | eqeltrd | |