Metamath Proof Explorer

Theorem invrcn

Description: The multiplicative inverse function is a continuous function from the unit group (that is, the nonzero numbers) to the field. (Contributed by Mario Carneiro, 5-Oct-2015)

		Ref	Expression
	Hypotheses	mulrcn.j	\|- J = ( TopOpen ` R )
		invrcn.i	\|- I = ( invr ` R )
		invrcn.u	\|- U = ( Unit ` R )
	Assertion	invrcn	\|- ( R e. TopDRing -> I e. ( ( J \|`t U ) Cn J ) )

Proof

Step	Hyp	Ref	Expression
1		mulrcn.j	\|- J = ( TopOpen ` R )
2		invrcn.i	\|- I = ( invr ` R )
3		invrcn.u	\|- U = ( Unit ` R )
4		tdrgtps	\|- ( R e. TopDRing -> R e. TopSp )
5	1	tpstop	\|- ( R e. TopSp -> J e. Top )
6		cnrest2r	\|- ( J e. Top -> ( ( J \|`t U ) Cn ( J \|`t U ) ) C_ ( ( J \|`t U ) Cn J ) )
7	4 5 6	3syl	\|- ( R e. TopDRing -> ( ( J \|`t U ) Cn ( J \|`t U ) ) C_ ( ( J \|`t U ) Cn J ) )
8	1 2 3	invrcn2	\|- ( R e. TopDRing -> I e. ( ( J \|`t U ) Cn ( J \|`t U ) ) )
9	7 8	sseldd	\|- ( R e. TopDRing -> I e. ( ( J \|`t U ) Cn J ) )