subginv

Description: The inverse of an element in a subgroup is the same as the inverse in the larger group. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	subg0.h	$⊢ H = G ↾_{𝑠} S$
	subginv.i	$⊢ I = {inv}_{g} (G)$
	subginv.j	$⊢ J = {inv}_{g} (H)$
Assertion	subginv	$⊢ (S \in SubGrp (G) \land X \in S) \to I (X) = J (X)$

Proof

Step	Hyp	Ref	Expression
1		subg0.h	$⊢ H = G ↾_{𝑠} S$
2		subginv.i	$⊢ I = {inv}_{g} (G)$
3		subginv.j	$⊢ J = {inv}_{g} (H)$
4	1	subggrp	$⊢ S \in SubGrp (G) \to H \in Grp$
5	1	subgbas	$⊢ S \in SubGrp (G) \to S = {Base}_{H}$
6	5	eleq2d	$⊢ S \in SubGrp (G) \to (X \in S \leftrightarrow X \in {Base}_{H})$
7	6	biimpa	$⊢ (S \in SubGrp (G) \land X \in S) \to X \in {Base}_{H}$
8		eqid	$⊢ {Base}_{H} = {Base}_{H}$
9		eqid	$⊢ +_{H} = +_{H}$
10		eqid	$⊢ 0_{H} = 0_{H}$
11	8 9 10 3	grprinv	$⊢ (H \in Grp \land X \in {Base}_{H}) \to X +_{H} J (X) = 0_{H}$
12	4 7 11	syl2an2r	$⊢ (S \in SubGrp (G) \land X \in S) \to X +_{H} J (X) = 0_{H}$
13		eqid	$⊢ +_{G} = +_{G}$
14	1 13	ressplusg	$⊢ S \in SubGrp (G) \to +_{G} = +_{H}$
15	14	adantr	$⊢ (S \in SubGrp (G) \land X \in S) \to +_{G} = +_{H}$
16	15	oveqd	$⊢ (S \in SubGrp (G) \land X \in S) \to X +_{G} J (X) = X +_{H} J (X)$
17		eqid	$⊢ 0_{G} = 0_{G}$
18	1 17	subg0	$⊢ S \in SubGrp (G) \to 0_{G} = 0_{H}$
19	18	adantr	$⊢ (S \in SubGrp (G) \land X \in S) \to 0_{G} = 0_{H}$
20	12 16 19	3eqtr4d	$⊢ (S \in SubGrp (G) \land X \in S) \to X +_{G} J (X) = 0_{G}$
21		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
22	21	adantr	$⊢ (S \in SubGrp (G) \land X \in S) \to G \in Grp$
23		eqid	$⊢ {Base}_{G} = {Base}_{G}$
24	23	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
25	24	sselda	$⊢ (S \in SubGrp (G) \land X \in S) \to X \in {Base}_{G}$
26	8 3	grpinvcl	$⊢ (H \in Grp \land X \in {Base}_{H}) \to J (X) \in {Base}_{H}$
27	26	ex	$⊢ H \in Grp \to (X \in {Base}_{H} \to J (X) \in {Base}_{H})$
28	4 27	syl	$⊢ S \in SubGrp (G) \to (X \in {Base}_{H} \to J (X) \in {Base}_{H})$
29	5	eleq2d	$⊢ S \in SubGrp (G) \to (J (X) \in S \leftrightarrow J (X) \in {Base}_{H})$
30	28 6 29	3imtr4d	$⊢ S \in SubGrp (G) \to (X \in S \to J (X) \in S)$
31	30	imp	$⊢ (S \in SubGrp (G) \land X \in S) \to J (X) \in S$
32	24	sselda	$⊢ (S \in SubGrp (G) \land J (X) \in S) \to J (X) \in {Base}_{G}$
33	31 32	syldan	$⊢ (S \in SubGrp (G) \land X \in S) \to J (X) \in {Base}_{G}$
34	23 13 17 2	grpinvid1	$⊢ (G \in Grp \land X \in {Base}_{G} \land J (X) \in {Base}_{G}) \to (I (X) = J (X) \leftrightarrow X +_{G} J (X) = 0_{G})$
35	22 25 33 34	syl3anc	$⊢ (S \in SubGrp (G) \land X \in S) \to (I (X) = J (X) \leftrightarrow X +_{G} J (X) = 0_{G})$
36	20 35	mpbird	$⊢ (S \in SubGrp (G) \land X \in S) \to I (X) = J (X)$

Metamath Proof Explorer

Theorem subginv

Proof