ablinvadd

Description: The inverse of an Abelian group operation. (Contributed by NM, 31-Mar-2014)

	Ref	Expression
Hypotheses	ablinvadd.b	$⊢ B = {Base}_{G}$
	ablinvadd.p	$⊢ \underset{˙}{+} = +_{G}$
	ablinvadd.n	$⊢ N = {inv}_{g} (G)$
Assertion	ablinvadd	$⊢ (G \in Abel \land X \in B \land Y \in B) \to N (X \underset{˙}{+} Y) = N (X) \underset{˙}{+} N (Y)$

Step	Hyp	Ref	Expression
1		ablinvadd.b	$⊢ B = {Base}_{G}$
2		ablinvadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		ablinvadd.n	$⊢ N = {inv}_{g} (G)$
4		ablgrp	$⊢ G \in Abel \to G \in Grp$
5	1 2 3	grpinvadd	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (X \underset{˙}{+} Y) = N (Y) \underset{˙}{+} N (X)$
6	4 5	syl3an1	$⊢ (G \in Abel \land X \in B \land Y \in B) \to N (X \underset{˙}{+} Y) = N (Y) \underset{˙}{+} N (X)$
7		simp1	$⊢ (G \in Abel \land X \in B \land Y \in B) \to G \in Abel$
8	4	3ad2ant1	$⊢ (G \in Abel \land X \in B \land Y \in B) \to G \in Grp$
9		simp2	$⊢ (G \in Abel \land X \in B \land Y \in B) \to X \in B$
10	1 3	grpinvcl	$⊢ (G \in Grp \land X \in B) \to N (X) \in B$
11	8 9 10	syl2anc	$⊢ (G \in Abel \land X \in B \land Y \in B) \to N (X) \in B$
12		simp3	$⊢ (G \in Abel \land X \in B \land Y \in B) \to Y \in B$
13	1 3	grpinvcl	$⊢ (G \in Grp \land Y \in B) \to N (Y) \in B$
14	8 12 13	syl2anc	$⊢ (G \in Abel \land X \in B \land Y \in B) \to N (Y) \in B$
15	1 2	ablcom	$⊢ (G \in Abel \land N (X) \in B \land N (Y) \in B) \to N (X) \underset{˙}{+} N (Y) = N (Y) \underset{˙}{+} N (X)$
16	7 11 14 15	syl3anc	$⊢ (G \in Abel \land X \in B \land Y \in B) \to N (X) \underset{˙}{+} N (Y) = N (Y) \underset{˙}{+} N (X)$
17	6 16	eqtr4d	$⊢ (G \in Abel \land X \in B \land Y \in B) \to N (X \underset{˙}{+} Y) = N (X) \underset{˙}{+} N (Y)$

Metamath Proof Explorer