Metamath Proof Explorer
Description: A subgroup is closed under multiplication. (Contributed by Mario
Carneiro, 2-Dec-2014) (Proof shortened by AV, 30-Mar-2025)
|
|
Ref |
Expression |
|
Hypothesis |
subrgmcl.p |
⊢ · = ( .r ‘ 𝑅 ) |
|
Assertion |
subrgmcl |
⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 · 𝑌 ) ∈ 𝐴 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
subrgmcl.p |
⊢ · = ( .r ‘ 𝑅 ) |
2 |
|
subrgsubrng |
⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ∈ ( SubRng ‘ 𝑅 ) ) |
3 |
1
|
subrngmcl |
⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 · 𝑌 ) ∈ 𝐴 ) |
4 |
2 3
|
syl3an1 |
⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 · 𝑌 ) ∈ 𝐴 ) |