ablsub4

Description: Commutative/associative subtraction law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by NM, 31-Mar-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ablsubadd.b	$⊢ B = {Base}_{G}$
2		ablsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		ablsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
4		ablgrp	$⊢ G \in Abel \to G \in Grp$
5	4	3ad2ant1	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to G \in Grp$
6		simp2l	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to X \in B$
7		simp2r	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Y \in B$
8	1 2	grpcl	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$
9	5 6 7 8	syl3anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to X \underset{˙}{+} Y \in B$
10		simp3l	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Z \in B$
11		simp3r	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to W \in B$
12	1 2	grpcl	$⊢ (G \in Grp \land Z \in B \land W \in B) \to Z \underset{˙}{+} W \in B$
13	5 10 11 12	syl3anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Z \underset{˙}{+} W \in B$
14		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
15	1 2 14 3	grpsubval	$⊢ (X \underset{˙}{+} Y \in B \land Z \underset{˙}{+} W \in B) \to (X \underset{˙}{+} Y) \underset{˙}{-} (Z \underset{˙}{+} W) = (X \underset{˙}{+} Y) \underset{˙}{+} {inv}_{g} (G) (Z \underset{˙}{+} W)$
16	9 13 15	syl2anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{-} (Z \underset{˙}{+} W) = (X \underset{˙}{+} Y) \underset{˙}{+} {inv}_{g} (G) (Z \underset{˙}{+} W)$
17		ablcmn	$⊢ G \in Abel \to G \in CMnd$
18	17	3ad2ant1	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to G \in CMnd$
19		simp2	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \in B \land Y \in B)$
20	1 14	grpinvcl	$⊢ (G \in Grp \land Z \in B) \to {inv}_{g} (G) (Z) \in B$
21	5 10 20	syl2anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to {inv}_{g} (G) (Z) \in B$
22	1 14	grpinvcl	$⊢ (G \in Grp \land W \in B) \to {inv}_{g} (G) (W) \in B$
23	5 11 22	syl2anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to {inv}_{g} (G) (W) \in B$
24	1 2	cmn4	$⊢ (G \in CMnd \land (X \in B \land Y \in B) \land ({inv}_{g} (G) (Z) \in B \land {inv}_{g} (G) (W) \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{+} ({inv}_{g} (G) (Z) \underset{˙}{+} {inv}_{g} (G) (W)) = (X \underset{˙}{+} {inv}_{g} (G) (Z)) \underset{˙}{+} (Y \underset{˙}{+} {inv}_{g} (G) (W))$
25	18 19 21 23 24	syl112anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{+} ({inv}_{g} (G) (Z) \underset{˙}{+} {inv}_{g} (G) (W)) = (X \underset{˙}{+} {inv}_{g} (G) (Z)) \underset{˙}{+} (Y \underset{˙}{+} {inv}_{g} (G) (W))$
26		simp1	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to G \in Abel$
27	1 2 14	ablinvadd	$⊢ (G \in Abel \land Z \in B \land W \in B) \to {inv}_{g} (G) (Z \underset{˙}{+} W) = {inv}_{g} (G) (Z) \underset{˙}{+} {inv}_{g} (G) (W)$
28	26 10 11 27	syl3anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to {inv}_{g} (G) (Z \underset{˙}{+} W) = {inv}_{g} (G) (Z) \underset{˙}{+} {inv}_{g} (G) (W)$
29	28	oveq2d	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{+} {inv}_{g} (G) (Z \underset{˙}{+} W) = (X \underset{˙}{+} Y) \underset{˙}{+} ({inv}_{g} (G) (Z) \underset{˙}{+} {inv}_{g} (G) (W))$
30	1 2 14 3	grpsubval	$⊢ (X \in B \land Z \in B) \to X \underset{˙}{-} Z = X \underset{˙}{+} {inv}_{g} (G) (Z)$
31	6 10 30	syl2anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to X \underset{˙}{-} Z = X \underset{˙}{+} {inv}_{g} (G) (Z)$
32	1 2 14 3	grpsubval	$⊢ (Y \in B \land W \in B) \to Y \underset{˙}{-} W = Y \underset{˙}{+} {inv}_{g} (G) (W)$
33	7 11 32	syl2anc	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Y \underset{˙}{-} W = Y \underset{˙}{+} {inv}_{g} (G) (W)$
34	31 33	oveq12d	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{-} Z) \underset{˙}{+} (Y \underset{˙}{-} W) = (X \underset{˙}{+} {inv}_{g} (G) (Z)) \underset{˙}{+} (Y \underset{˙}{+} {inv}_{g} (G) (W))$
35	25 29 34	3eqtr4d	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{+} {inv}_{g} (G) (Z \underset{˙}{+} W) = (X \underset{˙}{-} Z) \underset{˙}{+} (Y \underset{˙}{-} W)$
36	16 35	eqtrd	$⊢ (G \in Abel \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{-} (Z \underset{˙}{+} W) = (X \underset{˙}{-} Z) \underset{˙}{+} (Y \underset{˙}{-} W)$

Metamath Proof Explorer

Theorem ablsub4

Proof