Metamath Proof Explorer

Theorem nrginvrcn

Description: The ring inverse function is continuous in a normed ring. (Note that this is true even in rings which are not division rings.) (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses nrginvrcn.x 
|- X = ( Base ` R )
nrginvrcn.u 
|- U = ( Unit ` R )
nrginvrcn.i 
|- I = ( invr ` R )
nrginvrcn.j 
|- J = ( TopOpen ` R )
Assertion nrginvrcn 
|- ( R e. NrmRing -> I e. ( ( J |`t U ) Cn ( J |`t U ) ) )

Proof

Step Hyp Ref Expression
1 nrginvrcn.x 
 |-  X = ( Base ` R )
2 nrginvrcn.u 
 |-  U = ( Unit ` R )
3 nrginvrcn.i 
 |-  I = ( invr ` R )
4 nrginvrcn.j 
 |-  J = ( TopOpen ` R )
5 nrgring 
 |-  ( R e. NrmRing -> R e. Ring )
6 eqid 
 |-  ( ( mulGrp ` R ) |`s U ) = ( ( mulGrp ` R ) |`s U )
7 2 6 unitgrp 
 |-  ( R e. Ring -> ( ( mulGrp ` R ) |`s U ) e. Grp )
8 2 6 unitgrpbas 
 |-  U = ( Base ` ( ( mulGrp ` R ) |`s U ) )
9 2 6 3 invrfval 
 |-  I = ( invg ` ( ( mulGrp ` R ) |`s U ) )
10 8 9 grpinvf 
 |-  ( ( ( mulGrp ` R ) |`s U ) e. Grp -> I : U --> U )
11 5 7 10 3syl 
 |-  ( R e. NrmRing -> I : U --> U )
12 1rp 
 |-  1 e. RR+
13 12 ne0ii 
 |-  RR+ =/= (/)
14 5 ad2antrr 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> R e. Ring )
15 1 2 unitss 
 |-  U C_ X
16 simplrl 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> x e. U )
17 15 16 sseldi 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> x e. X )
18 simpr 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> y e. U )
19 15 18 sseldi 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> y e. X )
20 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
21 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
22 1 20 21 ring1eq0 
 |-  ( ( R e. Ring /\ x e. X /\ y e. X ) -> ( ( 1r ` R ) = ( 0g ` R ) -> x = y ) )
23 14 17 19 22 syl3anc 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> ( ( 1r ` R ) = ( 0g ` R ) -> x = y ) )
24 eqid 
 |-  ( I ` y ) = ( I ` y )
25 nrgngp 
 |-  ( R e. NrmRing -> R e. NrmGrp )
26 ngpms 
 |-  ( R e. NrmGrp -> R e. MetSp )
27 msxms 
 |-  ( R e. MetSp -> R e. *MetSp )
28 25 26 27 3syl 
 |-  ( R e. NrmRing -> R e. *MetSp )
29 28 ad2antrr 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> R e. *MetSp )
30 11 adantr 
 |-  ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) -> I : U --> U )
31 30 ffvelrnda 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> ( I ` y ) e. U )
32 15 31 sseldi 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> ( I ` y ) e. X )
33 eqid 
 |-  ( dist ` R ) = ( dist ` R )
34 1 33 xmseq0 
 |-  ( ( R e. *MetSp /\ ( I ` y ) e. X /\ ( I ` y ) e. X ) -> ( ( ( I ` y ) ( dist ` R ) ( I ` y ) ) = 0 <-> ( I ` y ) = ( I ` y ) ) )
35 29 32 32 34 syl3anc 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> ( ( ( I ` y ) ( dist ` R ) ( I ` y ) ) = 0 <-> ( I ` y ) = ( I ` y ) ) )
36 24 35 mpbiri 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> ( ( I ` y ) ( dist ` R ) ( I ` y ) ) = 0 )
37 simplrr 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> r e. RR+ )
38 37 rpgt0d 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> 0 < r )
39 36 38 eqbrtrd 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> ( ( I ` y ) ( dist ` R ) ( I ` y ) ) < r )
40 fveq2 
 |-  ( x = y -> ( I ` x ) = ( I ` y ) )
41 40 oveq1d 
 |-  ( x = y -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) = ( ( I ` y ) ( dist ` R ) ( I ` y ) ) )
42 41 breq1d 
 |-  ( x = y -> ( ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r <-> ( ( I ` y ) ( dist ` R ) ( I ` y ) ) < r ) )
43 39 42 syl5ibrcom 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> ( x = y -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r ) )
44 23 43 syld 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> ( ( 1r ` R ) = ( 0g ` R ) -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r ) )
45 44 imp 
 |-  ( ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) /\ ( 1r ` R ) = ( 0g ` R ) ) -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r )
46 45 an32s 
 |-  ( ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ ( 1r ` R ) = ( 0g ` R ) ) /\ y e. U ) -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r )
47 46 a1d 
 |-  ( ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ ( 1r ` R ) = ( 0g ` R ) ) /\ y e. U ) -> ( ( x ( dist ` R ) y ) < s -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r ) )
48 47 ralrimiva 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ ( 1r ` R ) = ( 0g ` R ) ) -> A. y e. U ( ( x ( dist ` R ) y ) < s -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r ) )
49 48 ralrimivw 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ ( 1r ` R ) = ( 0g ` R ) ) -> A. s e. RR+ A. y e. U ( ( x ( dist ` R ) y ) < s -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r ) )
50 r19.2z 
 |-  ( ( RR+ =/= (/) /\ A. s e. RR+ A. y e. U ( ( x ( dist ` R ) y ) < s -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r ) ) -> E. s e. RR+ A. y e. U ( ( x ( dist ` R ) y ) < s -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r ) )
51 13 49 50 sylancr 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ ( 1r ` R ) = ( 0g ` R ) ) -> E. s e. RR+ A. y e. U ( ( x ( dist ` R ) y ) < s -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r ) )
52 eqid 
 |-  ( norm ` R ) = ( norm ` R )
53 simpll 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> R e. NrmRing )
54 5 ad2antrr 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> R e. Ring )
55 simpr 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( 1r ` R ) =/= ( 0g ` R ) )
56 20 21 isnzr 
 |-  ( R e. NzRing <-> ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) )
57 54 55 56 sylanbrc 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> R e. NzRing )
58 simplrl 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> x e. U )
59 simplrr 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> r e. RR+ )
60 eqid 
 |-  ( if ( 1 <_ ( ( ( norm ` R ) ` x ) x. r ) , 1 , ( ( ( norm ` R ) ` x ) x. r ) ) x. ( ( ( norm ` R ) ` x ) / 2 ) ) = ( if ( 1 <_ ( ( ( norm ` R ) ` x ) x. r ) , 1 , ( ( ( norm ` R ) ` x ) x. r ) ) x. ( ( ( norm ` R ) ` x ) / 2 ) )
61 1 2 3 52 33 53 57 58 59 60 nrginvrcnlem 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> E. s e. RR+ A. y e. U ( ( x ( dist ` R ) y ) < s -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r ) )
62 51 61 pm2.61dane 
 |-  ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) -> E. s e. RR+ A. y e. U ( ( x ( dist ` R ) y ) < s -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r ) )
63 16 18 ovresd 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> ( x ( ( dist ` R ) |` ( U X. U ) ) y ) = ( x ( dist ` R ) y ) )
64 63 breq1d 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> ( ( x ( ( dist ` R ) |` ( U X. U ) ) y ) < s <-> ( x ( dist ` R ) y ) < s ) )
65 simpl 
 |-  ( ( x e. U /\ r e. RR+ ) -> x e. U )
66 ffvelrn 
 |-  ( ( I : U --> U /\ x e. U ) -> ( I ` x ) e. U )
67 11 65 66 syl2an 
 |-  ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) -> ( I ` x ) e. U )
68 67 adantr 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> ( I ` x ) e. U )
69 68 31 ovresd 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> ( ( I ` x ) ( ( dist ` R ) |` ( U X. U ) ) ( I ` y ) ) = ( ( I ` x ) ( dist ` R ) ( I ` y ) ) )
70 69 breq1d 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> ( ( ( I ` x ) ( ( dist ` R ) |` ( U X. U ) ) ( I ` y ) ) < r <-> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r ) )
71 64 70 imbi12d 
 |-  ( ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) /\ y e. U ) -> ( ( ( x ( ( dist ` R ) |` ( U X. U ) ) y ) < s -> ( ( I ` x ) ( ( dist ` R ) |` ( U X. U ) ) ( I ` y ) ) < r ) <-> ( ( x ( dist ` R ) y ) < s -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r ) ) )
72 71 ralbidva 
 |-  ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) -> ( A. y e. U ( ( x ( ( dist ` R ) |` ( U X. U ) ) y ) < s -> ( ( I ` x ) ( ( dist ` R ) |` ( U X. U ) ) ( I ` y ) ) < r ) <-> A. y e. U ( ( x ( dist ` R ) y ) < s -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r ) ) )
73 72 rexbidv 
 |-  ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) -> ( E. s e. RR+ A. y e. U ( ( x ( ( dist ` R ) |` ( U X. U ) ) y ) < s -> ( ( I ` x ) ( ( dist ` R ) |` ( U X. U ) ) ( I ` y ) ) < r ) <-> E. s e. RR+ A. y e. U ( ( x ( dist ` R ) y ) < s -> ( ( I ` x ) ( dist ` R ) ( I ` y ) ) < r ) ) )
74 62 73 mpbird 
 |-  ( ( R e. NrmRing /\ ( x e. U /\ r e. RR+ ) ) -> E. s e. RR+ A. y e. U ( ( x ( ( dist ` R ) |` ( U X. U ) ) y ) < s -> ( ( I ` x ) ( ( dist ` R ) |` ( U X. U ) ) ( I ` y ) ) < r ) )
75 74 ralrimivva 
 |-  ( R e. NrmRing -> A. x e. U A. r e. RR+ E. s e. RR+ A. y e. U ( ( x ( ( dist ` R ) |` ( U X. U ) ) y ) < s -> ( ( I ` x ) ( ( dist ` R ) |` ( U X. U ) ) ( I ` y ) ) < r ) )
76 xpss12 
 |-  ( ( U C_ X /\ U C_ X ) -> ( U X. U ) C_ ( X X. X ) )
77 15 15 76 mp2an 
 |-  ( U X. U ) C_ ( X X. X )
78 resabs1 
 |-  ( ( U X. U ) C_ ( X X. X ) -> ( ( ( dist ` R ) |` ( X X. X ) ) |` ( U X. U ) ) = ( ( dist ` R ) |` ( U X. U ) ) )
79 77 78 ax-mp 
 |-  ( ( ( dist ` R ) |` ( X X. X ) ) |` ( U X. U ) ) = ( ( dist ` R ) |` ( U X. U ) )
80 eqid 
 |-  ( ( dist ` R ) |` ( X X. X ) ) = ( ( dist ` R ) |` ( X X. X ) )
81 1 80 xmsxmet 
 |-  ( R e. *MetSp -> ( ( dist ` R ) |` ( X X. X ) ) e. ( *Met ` X ) )
82 25 26 27 81 4syl 
 |-  ( R e. NrmRing -> ( ( dist ` R ) |` ( X X. X ) ) e. ( *Met ` X ) )
83 xmetres2 
 |-  ( ( ( ( dist ` R ) |` ( X X. X ) ) e. ( *Met ` X ) /\ U C_ X ) -> ( ( ( dist ` R ) |` ( X X. X ) ) |` ( U X. U ) ) e. ( *Met ` U ) )
84 82 15 83 sylancl 
 |-  ( R e. NrmRing -> ( ( ( dist ` R ) |` ( X X. X ) ) |` ( U X. U ) ) e. ( *Met ` U ) )
85 79 84 eqeltrrid 
 |-  ( R e. NrmRing -> ( ( dist ` R ) |` ( U X. U ) ) e. ( *Met ` U ) )
86 eqid 
 |-  ( MetOpen ` ( ( dist ` R ) |` ( U X. U ) ) ) = ( MetOpen ` ( ( dist ` R ) |` ( U X. U ) ) )
87 86 86 metcn 
 |-  ( ( ( ( dist ` R ) |` ( U X. U ) ) e. ( *Met ` U ) /\ ( ( dist ` R ) |` ( U X. U ) ) e. ( *Met ` U ) ) -> ( I e. ( ( MetOpen ` ( ( dist ` R ) |` ( U X. U ) ) ) Cn ( MetOpen ` ( ( dist ` R ) |` ( U X. U ) ) ) ) <-> ( I : U --> U /\ A. x e. U A. r e. RR+ E. s e. RR+ A. y e. U ( ( x ( ( dist ` R ) |` ( U X. U ) ) y ) < s -> ( ( I ` x ) ( ( dist ` R ) |` ( U X. U ) ) ( I ` y ) ) < r ) ) ) )
88 85 85 87 syl2anc 
 |-  ( R e. NrmRing -> ( I e. ( ( MetOpen ` ( ( dist ` R ) |` ( U X. U ) ) ) Cn ( MetOpen ` ( ( dist ` R ) |` ( U X. U ) ) ) ) <-> ( I : U --> U /\ A. x e. U A. r e. RR+ E. s e. RR+ A. y e. U ( ( x ( ( dist ` R ) |` ( U X. U ) ) y ) < s -> ( ( I ` x ) ( ( dist ` R ) |` ( U X. U ) ) ( I ` y ) ) < r ) ) ) )
89 11 75 88 mpbir2and 
 |-  ( R e. NrmRing -> I e. ( ( MetOpen ` ( ( dist ` R ) |` ( U X. U ) ) ) Cn ( MetOpen ` ( ( dist ` R ) |` ( U X. U ) ) ) ) )
90 4 1 80 mstopn 
 |-  ( R e. MetSp -> J = ( MetOpen ` ( ( dist ` R ) |` ( X X. X ) ) ) )
91 25 26 90 3syl 
 |-  ( R e. NrmRing -> J = ( MetOpen ` ( ( dist ` R ) |` ( X X. X ) ) ) )
92 91 oveq1d 
 |-  ( R e. NrmRing -> ( J |`t U ) = ( ( MetOpen ` ( ( dist ` R ) |` ( X X. X ) ) ) |`t U ) )
93 79 eqcomi 
 |-  ( ( dist ` R ) |` ( U X. U ) ) = ( ( ( dist ` R ) |` ( X X. X ) ) |` ( U X. U ) )
94 eqid 
 |-  ( MetOpen ` ( ( dist ` R ) |` ( X X. X ) ) ) = ( MetOpen ` ( ( dist ` R ) |` ( X X. X ) ) )
95 93 94 86 metrest 
 |-  ( ( ( ( dist ` R ) |` ( X X. X ) ) e. ( *Met ` X ) /\ U C_ X ) -> ( ( MetOpen ` ( ( dist ` R ) |` ( X X. X ) ) ) |`t U ) = ( MetOpen ` ( ( dist ` R ) |` ( U X. U ) ) ) )
96 82 15 95 sylancl 
 |-  ( R e. NrmRing -> ( ( MetOpen ` ( ( dist ` R ) |` ( X X. X ) ) ) |`t U ) = ( MetOpen ` ( ( dist ` R ) |` ( U X. U ) ) ) )
97 92 96 eqtrd 
 |-  ( R e. NrmRing -> ( J |`t U ) = ( MetOpen ` ( ( dist ` R ) |` ( U X. U ) ) ) )
98 97 97 oveq12d 
 |-  ( R e. NrmRing -> ( ( J |`t U ) Cn ( J |`t U ) ) = ( ( MetOpen ` ( ( dist ` R ) |` ( U X. U ) ) ) Cn ( MetOpen ` ( ( dist ` R ) |` ( U X. U ) ) ) ) )
99 89 98 eleqtrrd 
 |-  ( R e. NrmRing -> I e. ( ( J |`t U ) Cn ( J |`t U ) ) )