Metamath Proof Explorer


Theorem ringcld

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 ( ๐œ‘ โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐ต )

Proof

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 โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐ต )