grpsubadd

Description: Relationship between group subtraction and addition. (Contributed by NM, 31-Mar-2014)

	Ref	Expression
Hypotheses	grpsubadd.b	$⊢ B = {Base}_{G}$
	grpsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
	grpsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
Assertion	grpsubadd	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Y = Z \leftrightarrow Z \underset{˙}{+} Y = X)$

Proof

Step	Hyp	Ref	Expression
1		grpsubadd.b	$⊢ B = {Base}_{G}$
2		grpsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
4		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
5	1 2 4 3	grpsubval	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{-} Y = X \underset{˙}{+} {inv}_{g} (G) (Y)$
6	5	3adant3	$⊢ (X \in B \land Y \in B \land Z \in B) \to X \underset{˙}{-} Y = X \underset{˙}{+} {inv}_{g} (G) (Y)$
7	6	adantl	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{-} Y = X \underset{˙}{+} {inv}_{g} (G) (Y)$
8	7	eqeq1d	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Y = Z \leftrightarrow X \underset{˙}{+} {inv}_{g} (G) (Y) = Z)$
9		simpl	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to G \in Grp$
10		simpr1	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
11	1 4	grpinvcl	$⊢ (G \in Grp \land Y \in B) \to {inv}_{g} (G) (Y) \in B$
12	11	3ad2antr2	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to {inv}_{g} (G) (Y) \in B$
13	1 2	grpcl	$⊢ (G \in Grp \land X \in B \land {inv}_{g} (G) (Y) \in B) \to X \underset{˙}{+} {inv}_{g} (G) (Y) \in B$
14	9 10 12 13	syl3anc	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{+} {inv}_{g} (G) (Y) \in B$
15		simpr3	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
16		simpr2	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
17	1 2	grprcan	$⊢ (G \in Grp \land (X \underset{˙}{+} {inv}_{g} (G) (Y) \in B \land Z \in B \land Y \in B)) \to ((X \underset{˙}{+} {inv}_{g} (G) (Y)) \underset{˙}{+} Y = Z \underset{˙}{+} Y \leftrightarrow X \underset{˙}{+} {inv}_{g} (G) (Y) = Z)$
18	9 14 15 16 17	syl13anc	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{+} {inv}_{g} (G) (Y)) \underset{˙}{+} Y = Z \underset{˙}{+} Y \leftrightarrow X \underset{˙}{+} {inv}_{g} (G) (Y) = Z)$
19	1 2	grpass	$⊢ (G \in Grp \land (X \in B \land {inv}_{g} (G) (Y) \in B \land Y \in B)) \to (X \underset{˙}{+} {inv}_{g} (G) (Y)) \underset{˙}{+} Y = X \underset{˙}{+} ({inv}_{g} (G) (Y) \underset{˙}{+} Y)$
20	9 10 12 16 19	syl13anc	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} {inv}_{g} (G) (Y)) \underset{˙}{+} Y = X \underset{˙}{+} ({inv}_{g} (G) (Y) \underset{˙}{+} Y)$
21		eqid	$⊢ 0_{G} = 0_{G}$
22	1 2 21 4	grplinv	$⊢ (G \in Grp \land Y \in B) \to {inv}_{g} (G) (Y) \underset{˙}{+} Y = 0_{G}$
23	22	3ad2antr2	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to {inv}_{g} (G) (Y) \underset{˙}{+} Y = 0_{G}$
24	23	oveq2d	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{+} ({inv}_{g} (G) (Y) \underset{˙}{+} Y) = X \underset{˙}{+} 0_{G}$
25	1 2 21	grprid	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{+} 0_{G} = X$
26	25	3ad2antr1	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{+} 0_{G} = X$
27	20 24 26	3eqtrd	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} {inv}_{g} (G) (Y)) \underset{˙}{+} Y = X$
28	27	eqeq1d	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{+} {inv}_{g} (G) (Y)) \underset{˙}{+} Y = Z \underset{˙}{+} Y \leftrightarrow X = Z \underset{˙}{+} Y)$
29	8 18 28	3bitr2d	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Y = Z \leftrightarrow X = Z \underset{˙}{+} Y)$
30		eqcom	$⊢ X = Z \underset{˙}{+} Y \leftrightarrow Z \underset{˙}{+} Y = X$
31	29 30	bitrdi	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Y = Z \leftrightarrow Z \underset{˙}{+} Y = X)$

Metamath Proof Explorer

Theorem grpsubadd

Proof