grpodivf

Description: Mapping for group division. (Contributed by NM, 10-Apr-2008) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

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	grpoinvcl	$⊢ (G \in GrpOp \land y \in X) \to inv (G) (y) \in X$
5	4	3adant2	$⊢ (G \in GrpOp \land x \in X \land y \in X) \to inv (G) (y) \in X$
6	1	grpocl	$⊢ (G \in GrpOp \land x \in X \land inv (G) (y) \in X) \to x G inv (G) (y) \in X$
7	5 6	syld3an3	$⊢ (G \in GrpOp \land x \in X \land y \in X) \to x G inv (G) (y) \in X$
8	7	3expib	$⊢ G \in GrpOp \to ((x \in X \land y \in X) \to x G inv (G) (y) \in X)$
9	8	ralrimivv	$⊢ G \in GrpOp \to \forall x \in X \forall y \in X x G inv (G) (y) \in X$
10		eqid	$⊢ (x \in X, y \in X ⟼ x G inv (G) (y)) = (x \in X, y \in X ⟼ x G inv (G) (y))$
11	10	fmpo	$⊢ \forall x \in X \forall y \in X x G inv (G) (y) \in X \leftrightarrow (x \in X, y \in X ⟼ x G inv (G) (y)) : X \times X ⟶ X$
12	9 11	sylib	$⊢ G \in GrpOp \to (x \in X, y \in X ⟼ x G inv (G) (y)) : X \times X ⟶ X$
13	1 3 2	grpodivfval	$⊢ G \in GrpOp \to D = (x \in X, y \in X ⟼ x G inv (G) (y))$
14	13	feq1d	$⊢ G \in GrpOp \to (D : X \times X ⟶ X \leftrightarrow (x \in X, y \in X ⟼ x G inv (G) (y)) : X \times X ⟶ X)$
15	12 14	mpbird	$⊢ G \in GrpOp \to D : X \times X ⟶ X$

Metamath Proof Explorer