grpoinvdiv

Description: Inverse of a group division. (Contributed by NM, 24-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpdiv.1	$⊢ X = ran G$
	grpdiv.2	$⊢ N = inv (G)$
	grpdiv.3	$⊢ D = /_{g} (G)$
Assertion	grpoinvdiv	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (A D B) = B D A$

Step	Hyp	Ref	Expression
1		grpdiv.1	$⊢ X = ran G$
2		grpdiv.2	$⊢ N = inv (G)$
3		grpdiv.3	$⊢ D = /_{g} (G)$
4	1 2 3	grpodivval	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A D B = A G N (B)$
5	4	fveq2d	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (A D B) = N (A G N (B))$
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	grpoinvop	$⊢ (G \in GrpOp \land A \in X \land N (B) \in X) \to N (A G N (B)) = N (N (B)) G N (A)$
9	7 8	syld3an3	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (A G N (B)) = N (N (B)) G N (A)$
10	1 2	grpo2inv	$⊢ (G \in GrpOp \land B \in X) \to N (N (B)) = B$
11	10	3adant2	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (N (B)) = B$
12	11	oveq1d	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (N (B)) G N (A) = B G N (A)$
13	1 2 3	grpodivval	$⊢ (G \in GrpOp \land B \in X \land A \in X) \to B D A = B G N (A)$
14	13	3com23	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to B D A = B G N (A)$
15	12 14	eqtr4d	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (N (B)) G N (A) = B D A$
16	5 9 15	3eqtrd	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (A D B) = B D A$

Metamath Proof Explorer