Theorem grpodivfval

Description: Group division (or subtraction) operation. (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	grpodivfval	|- ( G e. GrpOp -> D = ( x e. X , y e. X |-> ( x G ( N ` y ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		grpdiv.1	|- X = ran G
2		grpdiv.2	|- N = ( inv ` G )
3		grpdiv.3	|- D = ( /g ` G )
4		rnexg	|- ( G e. GrpOp -> ran G e. _V )
5	1 4	eqeltrid	|- ( G e. GrpOp -> X e. _V )
6		mpoexga	|- ( ( X e. _V /\ X e. _V ) -> ( x e. X , y e. X |-> ( x G ( N ` y ) ) ) e. _V )
7	5 5 6	syl2anc	|- ( G e. GrpOp -> ( x e. X , y e. X |-> ( x G ( N ` y ) ) ) e. _V )
8		rneq	|- ( g = G -> ran g = ran G )
9	8 1	eqtr4di	|- ( g = G -> ran g = X )
10		id	|- ( g = G -> g = G )
11		eqidd	|- ( g = G -> x = x )
12		fveq2	|- ( g = G -> ( inv ` g ) = ( inv ` G ) )
13	12 2	eqtr4di	|- ( g = G -> ( inv ` g ) = N )
14	13	fveq1d	|- ( g = G -> ( ( inv ` g ) ` y ) = ( N ` y ) )
15	10 11 14	oveq123d	|- ( g = G -> ( x g ( ( inv ` g ) ` y ) ) = ( x G ( N ` y ) ) )
16	9 9 15	mpoeq123dv	|- ( g = G -> ( x e. ran g , y e. ran g |-> ( x g ( ( inv ` g ) ` y ) ) ) = ( x e. X , y e. X |-> ( x G ( N ` y ) ) ) )
17		df-gdiv	|- /g = ( g e. GrpOp |-> ( x e. ran g , y e. ran g |-> ( x g ( ( inv ` g ) ` y ) ) ) )
18	16 17	fvmptg	|- ( ( G e. GrpOp /\ ( x e. X , y e. X |-> ( x G ( N ` y ) ) ) e. _V ) -> ( /g ` G ) = ( x e. X , y e. X |-> ( x G ( N ` y ) ) ) )
19	7 18	mpdan	|- ( G e. GrpOp -> ( /g ` G ) = ( x e. X , y e. X |-> ( x G ( N ` y ) ) ) )
20	3 19	eqtrid	|- ( G e. GrpOp -> D = ( x e. X , y e. X |-> ( x G ( N ` y ) ) ) )