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 = {inv}_{r} (R)$
	nrginvrcn.j	$⊢ J = TopOpen (R)$
Assertion	nrginvrcn	$⊢ R \in NrmRing \to I \in ((J ↾_{𝑡} U) Cn (J ↾_{𝑡} U))$

Proof

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

Metamath Proof Explorer

Theorem nrginvrcn

Proof