grpoinvop

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) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpasscan1.1	$⊢ X = ran G$
	grpasscan1.2	$⊢ N = inv (G)$
Assertion	grpoinvop	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (A G B) = N (B) G N (A)$

Proof

Step	Hyp	Ref	Expression
1		grpasscan1.1	$⊢ X = ran G$
2		grpasscan1.2	$⊢ N = inv (G)$
3		simp1	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to G \in GrpOp$
4		simp2	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A \in X$
5		simp3	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to B \in X$
6	1 2	grpoinvcl	$⊢ (G \in GrpOp \land B \in X) \to N (B) \in X$
7	6	3adant2	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (B) \in X$
8	1 2	grpoinvcl	$⊢ (G \in GrpOp \land A \in X) \to N (A) \in X$
9	8	3adant3	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (A) \in X$
10	1	grpocl	$⊢ (G \in GrpOp \land N (B) \in X \land N (A) \in X) \to N (B) G N (A) \in X$
11	3 7 9 10	syl3anc	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (B) G N (A) \in X$
12	1	grpoass	$⊢ (G \in GrpOp \land (A \in X \land B \in X \land N (B) G N (A) \in X)) \to (A G B) G (N (B) G N (A)) = A G (B G (N (B) G N (A)))$
13	3 4 5 11 12	syl13anc	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (A G B) G (N (B) G N (A)) = A G (B G (N (B) G N (A)))$
14		eqid	$⊢ GId (G) = GId (G)$
15	1 14 2	grporinv	$⊢ (G \in GrpOp \land B \in X) \to B G N (B) = GId (G)$
16	15	3adant2	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to B G N (B) = GId (G)$
17	16	oveq1d	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (B G N (B)) G N (A) = GId (G) G N (A)$
18	1	grpoass	$⊢ (G \in GrpOp \land (B \in X \land N (B) \in X \land N (A) \in X)) \to (B G N (B)) G N (A) = B G (N (B) G N (A))$
19	3 5 7 9 18	syl13anc	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (B G N (B)) G N (A) = B G (N (B) G N (A))$
20	1 14	grpolid	$⊢ (G \in GrpOp \land N (A) \in X) \to GId (G) G N (A) = N (A)$
21	8 20	syldan	$⊢ (G \in GrpOp \land A \in X) \to GId (G) G N (A) = N (A)$
22	21	3adant3	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to GId (G) G N (A) = N (A)$
23	17 19 22	3eqtr3d	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to B G (N (B) G N (A)) = N (A)$
24	23	oveq2d	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A G (B G (N (B) G N (A))) = A G N (A)$
25	1 14 2	grporinv	$⊢ (G \in GrpOp \land A \in X) \to A G N (A) = GId (G)$
26	25	3adant3	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A G N (A) = GId (G)$
27	13 24 26	3eqtrd	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (A G B) G (N (B) G N (A)) = GId (G)$
28	1	grpocl	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A G B \in X$
29	1 14 2	grpoinvid1	$⊢ (G \in GrpOp \land A G B \in X \land N (B) G N (A) \in X) \to (N (A G B) = N (B) G N (A) \leftrightarrow (A G B) G (N (B) G N (A)) = GId (G))$
30	3 28 11 29	syl3anc	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (N (A G B) = N (B) G N (A) \leftrightarrow (A G B) G (N (B) G N (A)) = GId (G))$
31	27 30	mpbird	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (A G B) = N (B) G N (A)$

Metamath Proof Explorer

Theorem grpoinvop

Proof