This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )