Description: Closure of the multiplication operation of a ring. (Contributed by SN, 29-Jul-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ringcld.b | |
|
ringcld.t | |
||
ringcld.r | |
||
ringcld.x | |
||
ringcld.y | |
||
Assertion | ringcld | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringcld.b | |
|
2 | ringcld.t | |
|
3 | ringcld.r | |
|
4 | ringcld.x | |
|
5 | ringcld.y | |
|
6 | 1 2 | ringcl | |
7 | 3 4 5 6 | syl3anc | |