subgsub

Description: The subtraction of elements in a subgroup is the same as subtraction in the group. (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Hypotheses	subgsubcl.p	$⊢ \underset{˙}{-} = -_{G}$
	subgsub.h	$⊢ H = G ↾_{𝑠} S$
	subgsub.n	$⊢ N = -_{H}$
Assertion	subgsub	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \underset{˙}{-} Y = X N Y$

Proof

Step	Hyp	Ref	Expression
1		subgsubcl.p	$⊢ \underset{˙}{-} = -_{G}$
2		subgsub.h	$⊢ H = G ↾_{𝑠} S$
3		subgsub.n	$⊢ N = -_{H}$
4		eqid	$⊢ +_{G} = +_{G}$
5	2 4	ressplusg	$⊢ S \in SubGrp (G) \to +_{G} = +_{H}$
6	5	3ad2ant1	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to +_{G} = +_{H}$
7		eqidd	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X = X$
8		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
9		eqid	$⊢ {inv}_{g} (H) = {inv}_{g} (H)$
10	2 8 9	subginv	$⊢ (S \in SubGrp (G) \land Y \in S) \to {inv}_{g} (G) (Y) = {inv}_{g} (H) (Y)$
11	10	3adant2	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to {inv}_{g} (G) (Y) = {inv}_{g} (H) (Y)$
12	6 7 11	oveq123d	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X +_{G} {inv}_{g} (G) (Y) = X +_{H} {inv}_{g} (H) (Y)$
13		eqid	$⊢ {Base}_{G} = {Base}_{G}$
14	13	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
15	14	3ad2ant1	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to S \subseteq {Base}_{G}$
16		simp2	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \in S$
17	15 16	sseldd	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \in {Base}_{G}$
18		simp3	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to Y \in S$
19	15 18	sseldd	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to Y \in {Base}_{G}$
20	13 4 8 1	grpsubval	$⊢ (X \in {Base}_{G} \land Y \in {Base}_{G}) \to X \underset{˙}{-} Y = X +_{G} {inv}_{g} (G) (Y)$
21	17 19 20	syl2anc	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \underset{˙}{-} Y = X +_{G} {inv}_{g} (G) (Y)$
22	2	subgbas	$⊢ S \in SubGrp (G) \to S = {Base}_{H}$
23	22	3ad2ant1	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to S = {Base}_{H}$
24	16 23	eleqtrd	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \in {Base}_{H}$
25	18 23	eleqtrd	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to Y \in {Base}_{H}$
26		eqid	$⊢ {Base}_{H} = {Base}_{H}$
27		eqid	$⊢ +_{H} = +_{H}$
28	26 27 9 3	grpsubval	$⊢ (X \in {Base}_{H} \land Y \in {Base}_{H}) \to X N Y = X +_{H} {inv}_{g} (H) (Y)$
29	24 25 28	syl2anc	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X N Y = X +_{H} {inv}_{g} (H) (Y)$
30	12 21 29	3eqtr4d	$⊢ (S \in SubGrp (G) \land X \in S \land Y \in S) \to X \underset{˙}{-} Y = X N Y$

Metamath Proof Explorer

Theorem subgsub

Proof