Metamath Proof Explorer

Theorem mgpval

Description: Value of the multiplication group operation. (Contributed by Mario Carneiro, 21-Dec-2014)

Ref Expression
Hypotheses mgpval.1 
|- M = ( mulGrp ` R )
mgpval.2 
|- .x. = ( .r ` R )
Assertion mgpval 
|- M = ( R sSet <. ( +g ` ndx ) , .x. >. )

Proof

Step Hyp Ref Expression
1 mgpval.1 
 |-  M = ( mulGrp ` R )
2 mgpval.2 
 |-  .x. = ( .r ` R )
3 id 
 |-  ( r = R -> r = R )
4 fveq2 
 |-  ( r = R -> ( .r ` r ) = ( .r ` R ) )
5 4 2 eqtr4di 
 |-  ( r = R -> ( .r ` r ) = .x. )
6 5 opeq2d 
 |-  ( r = R -> <. ( +g ` ndx ) , ( .r ` r ) >. = <. ( +g ` ndx ) , .x. >. )
7 3 6 oveq12d 
 |-  ( r = R -> ( r sSet <. ( +g ` ndx ) , ( .r ` r ) >. ) = ( R sSet <. ( +g ` ndx ) , .x. >. ) )
8 df-mgp 
 |-  mulGrp = ( r e. _V |-> ( r sSet <. ( +g ` ndx ) , ( .r ` r ) >. ) )
9 ovex 
 |-  ( R sSet <. ( +g ` ndx ) , .x. >. ) e. _V
10 7 8 9 fvmpt 
 |-  ( R e. _V -> ( mulGrp ` R ) = ( R sSet <. ( +g ` ndx ) , .x. >. ) )
11 fvprc 
 |-  ( -. R e. _V -> ( mulGrp ` R ) = (/) )
12 reldmsets 
 |-  Rel dom sSet
13 12 ovprc1 
 |-  ( -. R e. _V -> ( R sSet <. ( +g ` ndx ) , .x. >. ) = (/) )
14 11 13 eqtr4d 
 |-  ( -. R e. _V -> ( mulGrp ` R ) = ( R sSet <. ( +g ` ndx ) , .x. >. ) )
15 10 14 pm2.61i 
 |-  ( mulGrp ` R ) = ( R sSet <. ( +g ` ndx ) , .x. >. )
16 1 15 eqtri 
 |-  M = ( R sSet <. ( +g ` ndx ) , .x. >. )