# Metamath Proof Explorer

## Theorem subgcl

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

Ref Expression
Hypothesis subgcl.p
Assertion subgcl

### Proof

Step Hyp Ref Expression
1 subgcl.p
2 eqid ${⊢}{G}{↾}_{𝑠}{S}={G}{↾}_{𝑠}{S}$
3 2 subggrp ${⊢}{S}\in \mathrm{SubGrp}\left({G}\right)\to {G}{↾}_{𝑠}{S}\in \mathrm{Grp}$
4 3 3ad2ant1 ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {X}\in {S}\wedge {Y}\in {S}\right)\to {G}{↾}_{𝑠}{S}\in \mathrm{Grp}$
5 simp2 ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {X}\in {S}\wedge {Y}\in {S}\right)\to {X}\in {S}$
6 2 subgbas ${⊢}{S}\in \mathrm{SubGrp}\left({G}\right)\to {S}={\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
7 6 3ad2ant1 ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {X}\in {S}\wedge {Y}\in {S}\right)\to {S}={\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
8 5 7 eleqtrd ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {X}\in {S}\wedge {Y}\in {S}\right)\to {X}\in {\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
9 simp3 ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {X}\in {S}\wedge {Y}\in {S}\right)\to {Y}\in {S}$
10 9 7 eleqtrd ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {X}\in {S}\wedge {Y}\in {S}\right)\to {Y}\in {\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
11 eqid ${⊢}{\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}={\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
12 eqid ${⊢}{+}_{\left({G}{↾}_{𝑠}{S}\right)}={+}_{\left({G}{↾}_{𝑠}{S}\right)}$
13 11 12 grpcl ${⊢}\left({G}{↾}_{𝑠}{S}\in \mathrm{Grp}\wedge {X}\in {\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}\wedge {Y}\in {\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}\right)\to {X}{+}_{\left({G}{↾}_{𝑠}{S}\right)}{Y}\in {\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
14 4 8 10 13 syl3anc ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {X}\in {S}\wedge {Y}\in {S}\right)\to {X}{+}_{\left({G}{↾}_{𝑠}{S}\right)}{Y}\in {\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
15 2 1 ressplusg