grpinvadd

Description: The inverse of the group operation reverses the arguments. Lemma 2.2.1(d) of Herstein p. 55. (Contributed by NM, 27-Oct-2006)

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

Proof

Step	Hyp	Ref	Expression
1		grpinvadd.b	$⊢ B = {Base}_{G}$
2		grpinvadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpinvadd.n	$⊢ N = {inv}_{g} (G)$
4		simp1	$⊢ (G \in Grp \land X \in B \land Y \in B) \to G \in Grp$
5		simp2	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \in B$
6		simp3	$⊢ (G \in Grp \land X \in B \land Y \in B) \to Y \in B$
7	1 3	grpinvcl	$⊢ (G \in Grp \land Y \in B) \to N (Y) \in B$
8	7	3adant2	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (Y) \in B$
9	1 3	grpinvcl	$⊢ (G \in Grp \land X \in B) \to N (X) \in B$
10	9	3adant3	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (X) \in B$
11	1 2	grpcl	$⊢ (G \in Grp \land N (Y) \in B \land N (X) \in B) \to N (Y) \underset{˙}{+} N (X) \in B$
12	4 8 10 11	syl3anc	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (Y) \underset{˙}{+} N (X) \in B$
13	1 2	grpass	$⊢ (G \in Grp \land (X \in B \land Y \in B \land N (Y) \underset{˙}{+} N (X) \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{+} (N (Y) \underset{˙}{+} N (X)) = X \underset{˙}{+} (Y \underset{˙}{+} (N (Y) \underset{˙}{+} N (X)))$
14	4 5 6 12 13	syl13anc	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (X \underset{˙}{+} Y) \underset{˙}{+} (N (Y) \underset{˙}{+} N (X)) = X \underset{˙}{+} (Y \underset{˙}{+} (N (Y) \underset{˙}{+} N (X)))$
15		eqid	$⊢ 0_{G} = 0_{G}$
16	1 2 15 3	grprinv	$⊢ (G \in Grp \land Y \in B) \to Y \underset{˙}{+} N (Y) = 0_{G}$
17	16	3adant2	$⊢ (G \in Grp \land X \in B \land Y \in B) \to Y \underset{˙}{+} N (Y) = 0_{G}$
18	17	oveq1d	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (Y \underset{˙}{+} N (Y)) \underset{˙}{+} N (X) = 0_{G} \underset{˙}{+} N (X)$
19	1 2	grpass	$⊢ (G \in Grp \land (Y \in B \land N (Y) \in B \land N (X) \in B)) \to (Y \underset{˙}{+} N (Y)) \underset{˙}{+} N (X) = Y \underset{˙}{+} (N (Y) \underset{˙}{+} N (X))$
20	4 6 8 10 19	syl13anc	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (Y \underset{˙}{+} N (Y)) \underset{˙}{+} N (X) = Y \underset{˙}{+} (N (Y) \underset{˙}{+} N (X))$
21	1 2 15	grplid	$⊢ (G \in Grp \land N (X) \in B) \to 0_{G} \underset{˙}{+} N (X) = N (X)$
22	4 10 21	syl2anc	$⊢ (G \in Grp \land X \in B \land Y \in B) \to 0_{G} \underset{˙}{+} N (X) = N (X)$
23	18 20 22	3eqtr3d	$⊢ (G \in Grp \land X \in B \land Y \in B) \to Y \underset{˙}{+} (N (Y) \underset{˙}{+} N (X)) = N (X)$
24	23	oveq2d	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} (Y \underset{˙}{+} (N (Y) \underset{˙}{+} N (X))) = X \underset{˙}{+} N (X)$
25	1 2 15 3	grprinv	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{+} N (X) = 0_{G}$
26	25	3adant3	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} N (X) = 0_{G}$
27	14 24 26	3eqtrd	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (X \underset{˙}{+} Y) \underset{˙}{+} (N (Y) \underset{˙}{+} N (X)) = 0_{G}$
28	1 2	grpcl	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$
29	1 2 15 3	grpinvid1	$⊢ (G \in Grp \land X \underset{˙}{+} Y \in B \land N (Y) \underset{˙}{+} N (X) \in B) \to (N (X \underset{˙}{+} Y) = N (Y) \underset{˙}{+} N (X) \leftrightarrow (X \underset{˙}{+} Y) \underset{˙}{+} (N (Y) \underset{˙}{+} N (X)) = 0_{G})$
30	4 28 12 29	syl3anc	$⊢ (G \in Grp \land X \in B \land Y \in B) \to (N (X \underset{˙}{+} Y) = N (Y) \underset{˙}{+} N (X) \leftrightarrow (X \underset{˙}{+} Y) \underset{˙}{+} (N (Y) \underset{˙}{+} N (X)) = 0_{G})$
31	27 30	mpbird	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (X \underset{˙}{+} Y) = N (Y) \underset{˙}{+} N (X)$

Metamath Proof Explorer

Theorem grpinvadd

Proof