Step |
Hyp |
Ref |
Expression |
1 |
|
mulrcn.j |
|- J = ( TopOpen ` R ) |
2 |
|
invrcn.i |
|- I = ( invr ` R ) |
3 |
|
invrcn.u |
|- U = ( Unit ` R ) |
4 |
|
eqid |
|- ( mulGrp ` R ) = ( mulGrp ` R ) |
5 |
4 3
|
tdrgunit |
|- ( R e. TopDRing -> ( ( mulGrp ` R ) |`s U ) e. TopGrp ) |
6 |
|
eqid |
|- ( ( mulGrp ` R ) |`s U ) = ( ( mulGrp ` R ) |`s U ) |
7 |
4 1
|
mgptopn |
|- J = ( TopOpen ` ( mulGrp ` R ) ) |
8 |
6 7
|
resstopn |
|- ( J |`t U ) = ( TopOpen ` ( ( mulGrp ` R ) |`s U ) ) |
9 |
3 6 2
|
invrfval |
|- I = ( invg ` ( ( mulGrp ` R ) |`s U ) ) |
10 |
8 9
|
tgpinv |
|- ( ( ( mulGrp ` R ) |`s U ) e. TopGrp -> I e. ( ( J |`t U ) Cn ( J |`t U ) ) ) |
11 |
5 10
|
syl |
|- ( R e. TopDRing -> I e. ( ( J |`t U ) Cn ( J |`t U ) ) ) |