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 e. GrpOp /\ A e. X /\ B e. X ) -> ( 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 e. GrpOp -> D = ( x e. X , y e. X |-> ( x G ( N ` y ) ) ) )
5	4	oveqd	|- ( G e. GrpOp -> ( A D B ) = ( A ( x e. X , y e. X |-> ( x G ( N ` y ) ) ) B ) )
6		oveq1	|- ( x = A -> ( x G ( N ` y ) ) = ( A G ( N ` y ) ) )
7		fveq2	|- ( y = B -> ( N ` y ) = ( N ` B ) )
8	7	oveq2d	|- ( y = B -> ( A G ( N ` y ) ) = ( A G ( N ` B ) ) )
9		eqid	|- ( x e. X , y e. X |-> ( x G ( N ` y ) ) ) = ( x e. X , y e. X |-> ( x G ( N ` y ) ) )
10		ovex	|- ( A G ( N ` B ) ) e. _V
11	6 8 9 10	ovmpo	|- ( ( A e. X /\ B e. X ) -> ( A ( x e. X , y e. X |-> ( x G ( N ` y ) ) ) B ) = ( A G ( N ` B ) ) )
12	5 11	sylan9eq	|- ( ( G e. GrpOp /\ ( A e. X /\ B e. X ) ) -> ( A D B ) = ( A G ( N ` B ) ) )
13	12	3impb	|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A D B ) = ( A G ( N ` B ) ) )