Theorem dvrcn

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

	Ref	Expression
Hypotheses	dvrcn.j	⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
	dvrcn.d	⊢ / = ( /r ‘ 𝑅 )
	dvrcn.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion	dvrcn	⊢ ( 𝑅 ∈ TopDRing → / ∈ ( ( 𝐽 ×t ( 𝐽 ↾t 𝑈 ) ) Cn 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		dvrcn.j	⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
2		dvrcn.d	⊢ / = ( /r ‘ 𝑅 )
3		dvrcn.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
6		eqid	⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
7	4 5 3 6 2	dvrfval	⊢ / = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑦 ) ) )
8		tdrgtrg	⊢ ( 𝑅 ∈ TopDRing → 𝑅 ∈ TopRing )
9		tdrgtps	⊢ ( 𝑅 ∈ TopDRing → 𝑅 ∈ TopSp )
10	4 1	istps	⊢ ( 𝑅 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑅 ) ) )
11	9 10	sylib	⊢ ( 𝑅 ∈ TopDRing → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑅 ) ) )
12	4 3	unitss	⊢ 𝑈 ⊆ ( Base ‘ 𝑅 )
13		resttopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑅 ) ) ∧ 𝑈 ⊆ ( Base ‘ 𝑅 ) ) → ( 𝐽 ↾t 𝑈 ) ∈ ( TopOn ‘ 𝑈 ) )
14	11 12 13	sylancl	⊢ ( 𝑅 ∈ TopDRing → ( 𝐽 ↾t 𝑈 ) ∈ ( TopOn ‘ 𝑈 ) )
15	11 14	cnmpt1st	⊢ ( 𝑅 ∈ TopDRing → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ 𝑈 ↦ 𝑥 ) ∈ ( ( 𝐽 ×t ( 𝐽 ↾t 𝑈 ) ) Cn 𝐽 ) )
16	11 14	cnmpt2nd	⊢ ( 𝑅 ∈ TopDRing → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ 𝑈 ↦ 𝑦 ) ∈ ( ( 𝐽 ×t ( 𝐽 ↾t 𝑈 ) ) Cn ( 𝐽 ↾t 𝑈 ) ) )
17	1 6 3	invrcn	⊢ ( 𝑅 ∈ TopDRing → ( invr ‘ 𝑅 ) ∈ ( ( 𝐽 ↾t 𝑈 ) Cn 𝐽 ) )
18	11 14 16 17	cnmpt21f	⊢ ( 𝑅 ∈ TopDRing → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ 𝑈 ↦ ( ( invr ‘ 𝑅 ) ‘ 𝑦 ) ) ∈ ( ( 𝐽 ×t ( 𝐽 ↾t 𝑈 ) ) Cn 𝐽 ) )
19	1 5 8 11 14 15 18	cnmpt2mulr	⊢ ( 𝑅 ∈ TopDRing → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑦 ) ) ) ∈ ( ( 𝐽 ×t ( 𝐽 ↾t 𝑈 ) ) Cn 𝐽 ) )
20	7 19	eqeltrid	⊢ ( 𝑅 ∈ TopDRing → / ∈ ( ( 𝐽 ×t ( 𝐽 ↾t 𝑈 ) ) Cn 𝐽 ) )