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 ⊢ 𝑋 = ( Base ‘ 𝑅 )
nrginvrcn.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
nrginvrcn.i ⊢ 𝐼 = ( invr ‘ 𝑅 )
nrginvrcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
Assertion nrginvrcn ( 𝑅 ∈ NrmRing → 𝐼 ∈ ( ( 𝐽 ↾t 𝑈 ) Cn ( 𝐽 ↾t 𝑈 ) ) )

Proof

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