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 ⁡ G
Assertion subginvcl ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S → I ⁡ X ∈ S

Proof

Step Hyp Ref Expression
1 subginvcl.i ⊢ I = inv g ⁡ G
2 eqid ⊢ G ↾ 𝑠 S = G ↾ 𝑠 S
3 2 subggrp ⊢ S ∈ SubGrp ⁡ G → G ↾ 𝑠 S ∈ Grp
4 simpr ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S → X ∈ S
5 2 subgbas ⊢ S ∈ SubGrp ⁡ G → S = Base G ↾ 𝑠 S
6 5 adantr ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S → S = Base G ↾ 𝑠 S
7 4 6 eleqtrd ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S → X ∈ Base G ↾ 𝑠 S
8 eqid ⊢ Base G ↾ 𝑠 S = Base G ↾ 𝑠 S
9 eqid ⊢ inv g ⁡ G ↾ 𝑠 S = inv g ⁡ G ↾ 𝑠 S
10 8 9 grpinvcl ⊢ G ↾ 𝑠 S ∈ Grp ∧ X ∈ Base G ↾ 𝑠 S → inv g ⁡ G ↾ 𝑠 S ⁡ X ∈ Base G ↾ 𝑠 S
11 3 7 10 syl2an2r ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S → inv g ⁡ G ↾ 𝑠 S ⁡ X ∈ Base G ↾ 𝑠 S
12 2 1 9 subginv ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S → I ⁡ X = inv g ⁡ G ↾ 𝑠 S ⁡ X
13 11 12 6 3eltr4d ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S → I ⁡ X ∈ S