# Metamath Proof Explorer

## Theorem subrgmcl

Description: A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypothesis subrgmcl.p
Assertion subrgmcl

### Proof

Step Hyp Ref Expression
1 subrgmcl.p
2 eqid ${⊢}{R}{↾}_{𝑠}{A}={R}{↾}_{𝑠}{A}$
3 2 subrgring ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {R}{↾}_{𝑠}{A}\in \mathrm{Ring}$
4 3 3ad2ant1 ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {A}\wedge {Y}\in {A}\right)\to {R}{↾}_{𝑠}{A}\in \mathrm{Ring}$
5 simp2 ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {A}\wedge {Y}\in {A}\right)\to {X}\in {A}$
6 2 subrgbas ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {A}={\mathrm{Base}}_{\left({R}{↾}_{𝑠}{A}\right)}$
7 6 3ad2ant1 ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {A}\wedge {Y}\in {A}\right)\to {A}={\mathrm{Base}}_{\left({R}{↾}_{𝑠}{A}\right)}$
8 5 7 eleqtrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {A}\wedge {Y}\in {A}\right)\to {X}\in {\mathrm{Base}}_{\left({R}{↾}_{𝑠}{A}\right)}$
9 simp3 ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {A}\wedge {Y}\in {A}\right)\to {Y}\in {A}$
10 9 7 eleqtrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {A}\wedge {Y}\in {A}\right)\to {Y}\in {\mathrm{Base}}_{\left({R}{↾}_{𝑠}{A}\right)}$
11 eqid ${⊢}{\mathrm{Base}}_{\left({R}{↾}_{𝑠}{A}\right)}={\mathrm{Base}}_{\left({R}{↾}_{𝑠}{A}\right)}$
12 eqid ${⊢}{\cdot }_{\left({R}{↾}_{𝑠}{A}\right)}={\cdot }_{\left({R}{↾}_{𝑠}{A}\right)}$
13 11 12 ringcl ${⊢}\left({R}{↾}_{𝑠}{A}\in \mathrm{Ring}\wedge {X}\in {\mathrm{Base}}_{\left({R}{↾}_{𝑠}{A}\right)}\wedge {Y}\in {\mathrm{Base}}_{\left({R}{↾}_{𝑠}{A}\right)}\right)\to {X}{\cdot }_{\left({R}{↾}_{𝑠}{A}\right)}{Y}\in {\mathrm{Base}}_{\left({R}{↾}_{𝑠}{A}\right)}$
14 4 8 10 13 syl3anc ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {X}\in {A}\wedge {Y}\in {A}\right)\to {X}{\cdot }_{\left({R}{↾}_{𝑠}{A}\right)}{Y}\in {\mathrm{Base}}_{\left({R}{↾}_{𝑠}{A}\right)}$
15 2 1 ressmulr