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