grponpcan

Description: Cancellation law for group division. ( npcan analog.) (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		grpdivf.1	$⊢ X = ran G$
2		grpdivf.3	$⊢ D = /_{g} (G)$
3		eqid	$⊢ inv (G) = inv (G)$
4	1 3 2	grpodivval	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A D B = A G inv (G) (B)$
5	4	oveq1d	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (A D B) G B = (A G inv (G) (B)) G B$
6		simp1	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to G \in GrpOp$
7		simp2	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A \in X$
8	1 3	grpoinvcl	$⊢ (G \in GrpOp \land B \in X) \to inv (G) (B) \in X$
9	8	3adant2	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to inv (G) (B) \in X$
10		simp3	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to B \in X$
11	1	grpoass	$⊢ (G \in GrpOp \land (A \in X \land inv (G) (B) \in X \land B \in X)) \to (A G inv (G) (B)) G B = A G (inv (G) (B) G B)$
12	6 7 9 10 11	syl13anc	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (A G inv (G) (B)) G B = A G (inv (G) (B) G B)$
13		eqid	$⊢ GId (G) = GId (G)$
14	1 13 3	grpolinv	$⊢ (G \in GrpOp \land B \in X) \to inv (G) (B) G B = GId (G)$
15	14	oveq2d	$⊢ (G \in GrpOp \land B \in X) \to A G (inv (G) (B) G B) = A G GId (G)$
16	15	3adant2	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A G (inv (G) (B) G B) = A G GId (G)$
17	1 13	grporid	$⊢ (G \in GrpOp \land A \in X) \to A G GId (G) = A$
18	17	3adant3	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A G GId (G) = A$
19	16 18	eqtrd	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A G (inv (G) (B) G B) = A$
20	12 19	eqtrd	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (A G inv (G) (B)) G B = A$
21	5 20	eqtrd	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (A D B) G B = A$

Metamath Proof Explorer

Theorem grponpcan

Proof