| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mgpval.1 |
|- M = ( mulGrp ` R ) |
| 2 |
|
mgpval.2 |
|- .x. = ( .r ` R ) |
| 3 |
2
|
fvexi |
|- .x. e. _V |
| 4 |
|
plusgid |
|- +g = Slot ( +g ` ndx ) |
| 5 |
4
|
setsid |
|- ( ( R e. _V /\ .x. e. _V ) -> .x. = ( +g ` ( R sSet <. ( +g ` ndx ) , .x. >. ) ) ) |
| 6 |
3 5
|
mpan2 |
|- ( R e. _V -> .x. = ( +g ` ( R sSet <. ( +g ` ndx ) , .x. >. ) ) ) |
| 7 |
1 2
|
mgpval |
|- M = ( R sSet <. ( +g ` ndx ) , .x. >. ) |
| 8 |
7
|
fveq2i |
|- ( +g ` M ) = ( +g ` ( R sSet <. ( +g ` ndx ) , .x. >. ) ) |
| 9 |
6 8
|
eqtr4di |
|- ( R e. _V -> .x. = ( +g ` M ) ) |
| 10 |
4
|
str0 |
|- (/) = ( +g ` (/) ) |
| 11 |
|
fvprc |
|- ( -. R e. _V -> ( .r ` R ) = (/) ) |
| 12 |
2 11
|
eqtrid |
|- ( -. R e. _V -> .x. = (/) ) |
| 13 |
|
fvprc |
|- ( -. R e. _V -> ( mulGrp ` R ) = (/) ) |
| 14 |
1 13
|
eqtrid |
|- ( -. R e. _V -> M = (/) ) |
| 15 |
14
|
fveq2d |
|- ( -. R e. _V -> ( +g ` M ) = ( +g ` (/) ) ) |
| 16 |
10 12 15
|
3eqtr4a |
|- ( -. R e. _V -> .x. = ( +g ` M ) ) |
| 17 |
9 16
|
pm2.61i |
|- .x. = ( +g ` M ) |