grpodivinv

Description: Group division by an inverse. (Contributed by NM, 15-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	grpodivinv	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A D N (B) = A G B$

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	grpoinvcl	$⊢ (G \in GrpOp \land B \in X) \to N (B) \in X$
5	4	3adant2	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (B) \in X$
6	1 2 3	grpodivval	$⊢ (G \in GrpOp \land A \in X \land N (B) \in X) \to A D N (B) = A G N (N (B))$
7	5 6	syld3an3	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A D N (B) = A G N (N (B))$
8	1 2	grpo2inv	$⊢ (G \in GrpOp \land B \in X) \to N (N (B)) = B$
9	8	3adant2	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to N (N (B)) = B$
10	9	oveq2d	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A G N (N (B)) = A G B$
11	7 10	eqtrd	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A D N (B) = A G B$

Metamath Proof Explorer