Theorem grpodivinv

Description: Group division by an inverse. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpdiv.1	|- X = ran G
	grpdiv.2	|- N = ( inv ` G )
	grpdiv.3	|- D = ( /g ` G )
Assertion	grpodivinv	|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A D ( N ` B ) ) = ( A G 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	grpoinvcl	|- ( ( G e. GrpOp /\ B e. X ) -> ( N ` B ) e. X )
5	4	3adant2	|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( N ` B ) e. X )
6	1 2 3	grpodivval	|- ( ( G e. GrpOp /\ A e. X /\ ( N ` B ) e. X ) -> ( A D ( N ` B ) ) = ( A G ( N ` ( N ` B ) ) ) )
7	5 6	syld3an3	|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A D ( N ` B ) ) = ( A G ( N ` ( N ` B ) ) ) )
8	1 2	grpo2inv	|- ( ( G e. GrpOp /\ B e. X ) -> ( N ` ( N ` B ) ) = B )
9	8	3adant2	|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( N ` ( N ` B ) ) = B )
10	9	oveq2d	|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A G ( N ` ( N ` B ) ) ) = ( A G B ) )
11	7 10	eqtrd	|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A D ( N ` B ) ) = ( A G B ) )