# Metamath Proof Explorer

## Theorem subginvcl

Description: The inverse of an element is closed in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypothesis subginvcl.i ${⊢}{I}={inv}_{g}\left({G}\right)$
Assertion subginvcl ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {X}\in {S}\right)\to {I}\left({X}\right)\in {S}$

### Proof

Step Hyp Ref Expression
1 subginvcl.i ${⊢}{I}={inv}_{g}\left({G}\right)$
2 eqid ${⊢}{G}{↾}_{𝑠}{S}={G}{↾}_{𝑠}{S}$
3 2 subggrp ${⊢}{S}\in \mathrm{SubGrp}\left({G}\right)\to {G}{↾}_{𝑠}{S}\in \mathrm{Grp}$
4 simpr ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {X}\in {S}\right)\to {X}\in {S}$
5 2 subgbas ${⊢}{S}\in \mathrm{SubGrp}\left({G}\right)\to {S}={\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
6 5 adantr ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {X}\in {S}\right)\to {S}={\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
7 4 6 eleqtrd ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {X}\in {S}\right)\to {X}\in {\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
8 eqid ${⊢}{\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}={\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
9 eqid ${⊢}{inv}_{g}\left({G}{↾}_{𝑠}{S}\right)={inv}_{g}\left({G}{↾}_{𝑠}{S}\right)$
10 8 9 grpinvcl ${⊢}\left({G}{↾}_{𝑠}{S}\in \mathrm{Grp}\wedge {X}\in {\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}\right)\to {inv}_{g}\left({G}{↾}_{𝑠}{S}\right)\left({X}\right)\in {\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
11 3 7 10 syl2an2r ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {X}\in {S}\right)\to {inv}_{g}\left({G}{↾}_{𝑠}{S}\right)\left({X}\right)\in {\mathrm{Base}}_{\left({G}{↾}_{𝑠}{S}\right)}$
12 2 1 9 subginv ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {X}\in {S}\right)\to {I}\left({X}\right)={inv}_{g}\left({G}{↾}_{𝑠}{S}\right)\left({X}\right)$
13 11 12 6 3eltr4d ${⊢}\left({S}\in \mathrm{SubGrp}\left({G}\right)\wedge {X}\in {S}\right)\to {I}\left({X}\right)\in {S}$