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

Metamath Proof Explorer

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