| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dvrcn.j |
|- J = ( TopOpen ` R ) |
| 2 |
|
dvrcn.d |
|- ./ = ( /r ` R ) |
| 3 |
|
dvrcn.u |
|- U = ( Unit ` R ) |
| 4 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
| 5 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
| 6 |
|
eqid |
|- ( invr ` R ) = ( invr ` R ) |
| 7 |
4 5 3 6 2
|
dvrfval |
|- ./ = ( x e. ( Base ` R ) , y e. U |-> ( x ( .r ` R ) ( ( invr ` R ) ` y ) ) ) |
| 8 |
|
tdrgtrg |
|- ( R e. TopDRing -> R e. TopRing ) |
| 9 |
|
tdrgtps |
|- ( R e. TopDRing -> R e. TopSp ) |
| 10 |
4 1
|
istps |
|- ( R e. TopSp <-> J e. ( TopOn ` ( Base ` R ) ) ) |
| 11 |
9 10
|
sylib |
|- ( R e. TopDRing -> J e. ( TopOn ` ( Base ` R ) ) ) |
| 12 |
4 3
|
unitss |
|- U C_ ( Base ` R ) |
| 13 |
|
resttopon |
|- ( ( J e. ( TopOn ` ( Base ` R ) ) /\ U C_ ( Base ` R ) ) -> ( J |`t U ) e. ( TopOn ` U ) ) |
| 14 |
11 12 13
|
sylancl |
|- ( R e. TopDRing -> ( J |`t U ) e. ( TopOn ` U ) ) |
| 15 |
11 14
|
cnmpt1st |
|- ( R e. TopDRing -> ( x e. ( Base ` R ) , y e. U |-> x ) e. ( ( J tX ( J |`t U ) ) Cn J ) ) |
| 16 |
11 14
|
cnmpt2nd |
|- ( R e. TopDRing -> ( x e. ( Base ` R ) , y e. U |-> y ) e. ( ( J tX ( J |`t U ) ) Cn ( J |`t U ) ) ) |
| 17 |
1 6 3
|
invrcn |
|- ( R e. TopDRing -> ( invr ` R ) e. ( ( J |`t U ) Cn J ) ) |
| 18 |
11 14 16 17
|
cnmpt21f |
|- ( R e. TopDRing -> ( x e. ( Base ` R ) , y e. U |-> ( ( invr ` R ) ` y ) ) e. ( ( J tX ( J |`t U ) ) Cn J ) ) |
| 19 |
1 5 8 11 14 15 18
|
cnmpt2mulr |
|- ( R e. TopDRing -> ( x e. ( Base ` R ) , y e. U |-> ( x ( .r ` R ) ( ( invr ` R ) ` y ) ) ) e. ( ( J tX ( J |`t U ) ) Cn J ) ) |
| 20 |
7 19
|
eqeltrid |
|- ( R e. TopDRing -> ./ e. ( ( J tX ( J |`t U ) ) Cn J ) ) |