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	$⊢ \underset{˙}{\times} = /_{r} (R)$
	dvrcn.u	$⊢ U = Unit (R)$
Assertion	dvrcn	$⊢ R \in TopDRing \to \underset{˙}{\times} \in ((J \times_{t} (J ↾_{𝑡} U)) Cn J)$

Step	Hyp	Ref	Expression
1		dvrcn.j	$⊢ J = TopOpen (R)$
2		dvrcn.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
3		dvrcn.u	$⊢ U = Unit (R)$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5		eqid	$⊢ \cdot_{R} = \cdot_{R}$
6		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
7	4 5 3 6 2	dvrfval	$⊢ \underset{˙}{\times} = (x \in {Base}_{R}, y \in U ⟼ x \cdot_{R} {inv}_{r} (R) (y))$
8		tdrgtrg	$⊢ R \in TopDRing \to R \in TopRing$
9		tdrgtps	$⊢ R \in TopDRing \to R \in TopSp$
10	4 1	istps	$⊢ R \in TopSp \leftrightarrow J \in TopOn ({Base}_{R})$
11	9 10	sylib	$⊢ R \in TopDRing \to J \in TopOn ({Base}_{R})$
12	4 3	unitss	$⊢ U \subseteq {Base}_{R}$
13		resttopon	$⊢ (J \in TopOn ({Base}_{R}) \land U \subseteq {Base}_{R}) \to J ↾_{𝑡} U \in TopOn (U)$
14	11 12 13	sylancl	$⊢ R \in TopDRing \to J ↾_{𝑡} U \in TopOn (U)$
15	11 14	cnmpt1st	$⊢ R \in TopDRing \to (x \in {Base}_{R}, y \in U ⟼ x) \in ((J \times_{t} (J ↾_{𝑡} U)) Cn J)$
16	11 14	cnmpt2nd	$⊢ R \in TopDRing \to (x \in {Base}_{R}, y \in U ⟼ y) \in ((J \times_{t} (J ↾_{𝑡} U)) Cn (J ↾_{𝑡} U))$
17	1 6 3	invrcn	$⊢ R \in TopDRing \to {inv}_{r} (R) \in ((J ↾_{𝑡} U) Cn J)$
18	11 14 16 17	cnmpt21f	$⊢ R \in TopDRing \to (x \in {Base}_{R}, y \in U ⟼ {inv}_{r} (R) (y)) \in ((J \times_{t} (J ↾_{𝑡} U)) Cn J)$
19	1 5 8 11 14 15 18	cnmpt2mulr	$⊢ R \in TopDRing \to (x \in {Base}_{R}, y \in U ⟼ x \cdot_{R} {inv}_{r} (R) (y)) \in ((J \times_{t} (J ↾_{𝑡} U)) Cn J)$
20	7 19	eqeltrid	$⊢ R \in TopDRing \to \underset{˙}{\times} \in ((J \times_{t} (J ↾_{𝑡} U)) Cn J)$

Metamath Proof Explorer