| Step |
Hyp |
Ref |
Expression |
| 1 |
|
invrfval.u |
|- U = ( Unit ` R ) |
| 2 |
|
invrfval.g |
|- G = ( ( mulGrp ` R ) |`s U ) |
| 3 |
|
invrfval.i |
|- I = ( invr ` R ) |
| 4 |
|
fveq2 |
|- ( r = R -> ( mulGrp ` r ) = ( mulGrp ` R ) ) |
| 5 |
|
fveq2 |
|- ( r = R -> ( Unit ` r ) = ( Unit ` R ) ) |
| 6 |
5 1
|
eqtr4di |
|- ( r = R -> ( Unit ` r ) = U ) |
| 7 |
4 6
|
oveq12d |
|- ( r = R -> ( ( mulGrp ` r ) |`s ( Unit ` r ) ) = ( ( mulGrp ` R ) |`s U ) ) |
| 8 |
7 2
|
eqtr4di |
|- ( r = R -> ( ( mulGrp ` r ) |`s ( Unit ` r ) ) = G ) |
| 9 |
8
|
fveq2d |
|- ( r = R -> ( invg ` ( ( mulGrp ` r ) |`s ( Unit ` r ) ) ) = ( invg ` G ) ) |
| 10 |
|
df-invr |
|- invr = ( r e. _V |-> ( invg ` ( ( mulGrp ` r ) |`s ( Unit ` r ) ) ) ) |
| 11 |
|
fvex |
|- ( invg ` G ) e. _V |
| 12 |
9 10 11
|
fvmpt |
|- ( R e. _V -> ( invr ` R ) = ( invg ` G ) ) |
| 13 |
|
fvprc |
|- ( -. R e. _V -> ( invr ` R ) = (/) ) |
| 14 |
|
base0 |
|- (/) = ( Base ` (/) ) |
| 15 |
|
eqid |
|- ( invg ` (/) ) = ( invg ` (/) ) |
| 16 |
14 15
|
grpinvfn |
|- ( invg ` (/) ) Fn (/) |
| 17 |
|
fn0 |
|- ( ( invg ` (/) ) Fn (/) <-> ( invg ` (/) ) = (/) ) |
| 18 |
16 17
|
mpbi |
|- ( invg ` (/) ) = (/) |
| 19 |
13 18
|
eqtr4di |
|- ( -. R e. _V -> ( invr ` R ) = ( invg ` (/) ) ) |
| 20 |
|
fvprc |
|- ( -. R e. _V -> ( mulGrp ` R ) = (/) ) |
| 21 |
20
|
oveq1d |
|- ( -. R e. _V -> ( ( mulGrp ` R ) |`s U ) = ( (/) |`s U ) ) |
| 22 |
2 21
|
eqtrid |
|- ( -. R e. _V -> G = ( (/) |`s U ) ) |
| 23 |
|
ress0 |
|- ( (/) |`s U ) = (/) |
| 24 |
22 23
|
eqtrdi |
|- ( -. R e. _V -> G = (/) ) |
| 25 |
24
|
fveq2d |
|- ( -. R e. _V -> ( invg ` G ) = ( invg ` (/) ) ) |
| 26 |
19 25
|
eqtr4d |
|- ( -. R e. _V -> ( invr ` R ) = ( invg ` G ) ) |
| 27 |
12 26
|
pm2.61i |
|- ( invr ` R ) = ( invg ` G ) |
| 28 |
3 27
|
eqtri |
|- I = ( invg ` G ) |