grpsubsub4

Description: Double group subtraction ( subsub4 analog). (Contributed by Mario Carneiro, 2-Dec-2014)

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

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	1 3	grpsubcl	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{-} Y \in B$
6	5	3adant3r3	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{-} Y \in B$
7		simpr3	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
8	1 2 3	grpnpcan	$⊢ (G \in Grp \land X \underset{˙}{-} Y \in B \land Z \in B) \to ((X \underset{˙}{-} Y) \underset{˙}{-} Z) \underset{˙}{+} Z = X \underset{˙}{-} Y$
9	4 6 7 8	syl3anc	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{-} Y) \underset{˙}{-} Z) \underset{˙}{+} Z = X \underset{˙}{-} Y$
10	9	oveq1d	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (((X \underset{˙}{-} Y) \underset{˙}{-} Z) \underset{˙}{+} Z) \underset{˙}{+} Y = (X \underset{˙}{-} Y) \underset{˙}{+} Y$
11	1 3	grpsubcl	$⊢ (G \in Grp \land X \underset{˙}{-} Y \in B \land Z \in B) \to (X \underset{˙}{-} Y) \underset{˙}{-} Z \in B$
12	4 6 7 11	syl3anc	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Y) \underset{˙}{-} Z \in B$
13		simpr2	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
14	1 2	grpass	$⊢ (G \in Grp \land ((X \underset{˙}{-} Y) \underset{˙}{-} Z \in B \land Z \in B \land Y \in B)) \to (((X \underset{˙}{-} Y) \underset{˙}{-} Z) \underset{˙}{+} Z) \underset{˙}{+} Y = ((X \underset{˙}{-} Y) \underset{˙}{-} Z) \underset{˙}{+} (Z \underset{˙}{+} Y)$
15	4 12 7 13 14	syl13anc	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (((X \underset{˙}{-} Y) \underset{˙}{-} Z) \underset{˙}{+} Z) \underset{˙}{+} Y = ((X \underset{˙}{-} Y) \underset{˙}{-} Z) \underset{˙}{+} (Z \underset{˙}{+} Y)$
16	1 2 3	grpnpcan	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (X \underset{˙}{-} Y) \underset{˙}{+} Y = X$
17	16	3adant3r3	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Y) \underset{˙}{+} Y = X$
18	10 15 17	3eqtr3d	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{-} Y) \underset{˙}{-} Z) \underset{˙}{+} (Z \underset{˙}{+} Y) = X$
19		simpr1	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
20	1 2	grpcl	$⊢ (G \in Grp \land Z \in B \land Y \in B) \to Z \underset{˙}{+} Y \in B$
21	4 7 13 20	syl3anc	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to Z \underset{˙}{+} Y \in B$
22	1 2 3	grpsubadd	$⊢ (G \in Grp \land (X \in B \land Z \underset{˙}{+} Y \in B \land (X \underset{˙}{-} Y) \underset{˙}{-} Z \in B)) \to (X \underset{˙}{-} (Z \underset{˙}{+} Y) = (X \underset{˙}{-} Y) \underset{˙}{-} Z \leftrightarrow ((X \underset{˙}{-} Y) \underset{˙}{-} Z) \underset{˙}{+} (Z \underset{˙}{+} Y) = X)$
23	4 19 21 12 22	syl13anc	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} (Z \underset{˙}{+} Y) = (X \underset{˙}{-} Y) \underset{˙}{-} Z \leftrightarrow ((X \underset{˙}{-} Y) \underset{˙}{-} Z) \underset{˙}{+} (Z \underset{˙}{+} Y) = X)$
24	18 23	mpbird	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{-} (Z \underset{˙}{+} Y) = (X \underset{˙}{-} Y) \underset{˙}{-} Z$
25	24	eqcomd	$⊢ (G \in Grp \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Y) \underset{˙}{-} Z = X \underset{˙}{-} (Z \underset{˙}{+} Y)$

Metamath Proof Explorer

Theorem grpsubsub4

Proof