grpaddsubass

Description: Associative-type law for group subtraction and addition. (Contributed by NM, 16-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		grpsubadd.b	$⊢ B = {Base}_{G}$
2		grpsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
4		simpl	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to G \in Grp$
5		simpr1	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
6		simpr2	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
7		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
8	1 7	grpinvcl	$⊢ (G \in Grp \land Z \in B) \to {inv}_{g} (G) (Z) \in B$
9	8	3ad2antr3	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to {inv}_{g} (G) (Z) \in B$
10	1 2	grpass	$⊢ (G \in Grp \land (X \in B \land Y \in B \land {inv}_{g} (G) (Z) \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{+} {inv}_{g} (G) (Z) = X \underset{˙}{+} (Y \underset{˙}{+} {inv}_{g} (G) (Z))$
11	4 5 6 9 10	syl13anc	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{+} {inv}_{g} (G) (Z) = X \underset{˙}{+} (Y \underset{˙}{+} {inv}_{g} (G) (Z))$
12	1 2	grpcl	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$
13	12	3adant3r3	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{+} Y \in B$
14		simpr3	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
15	1 2 7 3	grpsubval	$⊢ (X \underset{˙}{+} Y \in B \land Z \in B) \to (X \underset{˙}{+} Y) \underset{˙}{-} Z = (X \underset{˙}{+} Y) \underset{˙}{+} {inv}_{g} (G) (Z)$
16	13 14 15	syl2anc	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{-} Z = (X \underset{˙}{+} Y) \underset{˙}{+} {inv}_{g} (G) (Z)$
17	1 2 7 3	grpsubval	$⊢ (Y \in B \land Z \in B) \to Y \underset{˙}{-} Z = Y \underset{˙}{+} {inv}_{g} (G) (Z)$
18	6 14 17	syl2anc	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{-} Z = Y \underset{˙}{+} {inv}_{g} (G) (Z)$
19	18	oveq2d	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{+} (Y \underset{˙}{-} Z) = X \underset{˙}{+} (Y \underset{˙}{+} {inv}_{g} (G) (Z))$
20	11 16 19	3eqtr4d	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{-} Z = X \underset{˙}{+} (Y \underset{˙}{-} Z)$

Metamath Proof Explorer

Theorem grpaddsubass

Proof