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

Metamath Proof Explorer

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