Metamath Proof Explorer

Theorem grpodivval

Description: Group division (or subtraction) operation value. (Contributed by NM, 15-Feb-2008) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

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

Proof

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	grpodivfval	$⊢ G \in GrpOp \to D = (x \in X, y \in X ⟼ x G N (y))$
5	4	oveqd	$⊢ G \in GrpOp \to A D B = A (x \in X, y \in X ⟼ x G N (y)) B$
6		oveq1	$⊢ x = A \to x G N (y) = A G N (y)$
7		fveq2	$⊢ y = B \to N (y) = N (B)$
8	7	oveq2d	$⊢ y = B \to A G N (y) = A G N (B)$
9		eqid	$⊢ (x \in X, y \in X ⟼ x G N (y)) = (x \in X, y \in X ⟼ x G N (y))$
10		ovex	$⊢ A G N (B) \in V$
11	6 8 9 10	ovmpo	$⊢ (A \in X \land B \in X) \to A (x \in X, y \in X ⟼ x G N (y)) B = A G N (B)$
12	5 11	sylan9eq	$⊢ (G \in GrpOp \land (A \in X \land B \in X)) \to A D B = A G N (B)$
13	12	3impb	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A D B = A G N (B)$