Theorem grpodivf

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

	Ref	Expression
Hypotheses	grpdivf.1	|- X = ran G
	grpdivf.3	|- D = ( /g ` G )
Assertion	grpodivf	|- ( G e. GrpOp -> D : ( X X. X ) --> X )

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	grpoinvcl	|- ( ( G e. GrpOp /\ y e. X ) -> ( ( inv ` G ) ` y ) e. X )
5	4	3adant2	|- ( ( G e. GrpOp /\ x e. X /\ y e. X ) -> ( ( inv ` G ) ` y ) e. X )
6	1	grpocl	|- ( ( G e. GrpOp /\ x e. X /\ ( ( inv ` G ) ` y ) e. X ) -> ( x G ( ( inv ` G ) ` y ) ) e. X )
7	5 6	syld3an3	|- ( ( G e. GrpOp /\ x e. X /\ y e. X ) -> ( x G ( ( inv ` G ) ` y ) ) e. X )
8	7	3expib	|- ( G e. GrpOp -> ( ( x e. X /\ y e. X ) -> ( x G ( ( inv ` G ) ` y ) ) e. X ) )
9	8	ralrimivv	|- ( G e. GrpOp -> A. x e. X A. y e. X ( x G ( ( inv ` G ) ` y ) ) e. X )
10		eqid	|- ( x e. X , y e. X |-> ( x G ( ( inv ` G ) ` y ) ) ) = ( x e. X , y e. X |-> ( x G ( ( inv ` G ) ` y ) ) )
11	10	fmpo	|- ( A. x e. X A. y e. X ( x G ( ( inv ` G ) ` y ) ) e. X <-> ( x e. X , y e. X |-> ( x G ( ( inv ` G ) ` y ) ) ) : ( X X. X ) --> X )
12	9 11	sylib	|- ( G e. GrpOp -> ( x e. X , y e. X |-> ( x G ( ( inv ` G ) ` y ) ) ) : ( X X. X ) --> X )
13	1 3 2	grpodivfval	|- ( G e. GrpOp -> D = ( x e. X , y e. X |-> ( x G ( ( inv ` G ) ` y ) ) ) )
14	13	feq1d	|- ( G e. GrpOp -> ( D : ( X X. X ) --> X <-> ( x e. X , y e. X |-> ( x G ( ( inv ` G ) ` y ) ) ) : ( X X. X ) --> X ) )
15	12 14	mpbird	|- ( G e. GrpOp -> D : ( X X. X ) --> X )