Metamath Proof Explorer

Theorem dvrcn

Description: The division function is continuous in a topological field. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses dvrcn.j 
|- J = ( TopOpen ` R )
dvrcn.d 
|- ./ = ( /r ` R )
dvrcn.u 
|- U = ( Unit ` R )
Assertion dvrcn 
|- ( R e. TopDRing -> ./ e. ( ( J tX ( J |`t U ) ) Cn J ) )

Proof

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 ) )