Metamath Proof Explorer


Theorem subrgmcl

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 A SubRing R X A Y A X · ˙ Y A

Proof

Step Hyp Ref Expression
1 subrgmcl.p · ˙ = R
2 subrgsubrng Could not format ( A e. ( SubRing ` R ) -> A e. ( SubRng ` R ) ) : No typesetting found for |- ( A e. ( SubRing ` R ) -> A e. ( SubRng ` R ) ) with typecode |-
3 1 subrngmcl Could not format ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A ) with typecode |-
4 2 3 syl3an1 A SubRing R X A Y A X · ˙ Y A