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 
|- .x. = ( .r ` R )
Assertion subrgmcl 
|- ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A )

Proof

Step Hyp Ref Expression
1 subrgmcl.p 
 |-  .x. = ( .r ` R )
2 subrgsubrng 
 |-  ( A e. ( SubRing ` R ) -> A e. ( SubRng ` R ) )
3 1 subrngmcl 
 |-  ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A )
4 2 3 syl3an1 
 |-  ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A )