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 \in SubGrp (G) \land X \in S) \to I (X) \in S$

Step	Hyp	Ref	Expression
1		subginvcl.i	$⊢ I = {inv}_{g} (G)$
2		eqid	$⊢ G ↾_{𝑠} S = G ↾_{𝑠} S$
3	2	subggrp	$⊢ S \in SubGrp (G) \to G ↾_{𝑠} S \in Grp$
4		simpr	$⊢ (S \in SubGrp (G) \land X \in S) \to X \in S$
5	2	subgbas	$⊢ S \in SubGrp (G) \to S = {Base}_{(G ↾_{𝑠} S)}$
6	5	adantr	$⊢ (S \in SubGrp (G) \land X \in S) \to S = {Base}_{(G ↾_{𝑠} S)}$
7	4 6	eleqtrd	$⊢ (S \in SubGrp (G) \land X \in S) \to X \in {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 \in Grp \land X \in {Base}_{(G ↾_{𝑠} S)}) \to {inv}_{g} (G ↾_{𝑠} S) (X) \in {Base}_{(G ↾_{𝑠} S)}$
11	3 7 10	syl2an2r	$⊢ (S \in SubGrp (G) \land X \in S) \to {inv}_{g} (G ↾_{𝑠} S) (X) \in {Base}_{(G ↾_{𝑠} S)}$
12	2 1 9	subginv	$⊢ (S \in SubGrp (G) \land X \in S) \to I (X) = {inv}_{g} (G ↾_{𝑠} S) (X)$
13	11 12 6	3eltr4d	$⊢ (S \in SubGrp (G) \land X \in S) \to I (X) \in S$

Metamath Proof Explorer