Theorem invrcn2

Description: The multiplicative inverse function is a continuous function from the unit group (that is, the nonzero numbers) to itself. (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	invrcn2	|- ( R e. TopDRing -> I e. ( ( J |`t U ) Cn ( J |`t U ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulrcn.j	|- J = ( TopOpen ` R )
2		invrcn.i	|- I = ( invr ` R )
3		invrcn.u	|- U = ( Unit ` R )
4		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
5	4 3	tdrgunit	|- ( R e. TopDRing -> ( ( mulGrp ` R ) |`s U ) e. TopGrp )
6		eqid	|- ( ( mulGrp ` R ) |`s U ) = ( ( mulGrp ` R ) |`s U )
7	4 1	mgptopn	|- J = ( TopOpen ` ( mulGrp ` R ) )
8	6 7	resstopn	|- ( J |`t U ) = ( TopOpen ` ( ( mulGrp ` R ) |`s U ) )
9	3 6 2	invrfval	|- I = ( invg ` ( ( mulGrp ` R ) |`s U ) )
10	8 9	tgpinv	|- ( ( ( mulGrp ` R ) |`s U ) e. TopGrp -> I e. ( ( J |`t U ) Cn ( J |`t U ) ) )
11	5 10	syl	|- ( R e. TopDRing -> I e. ( ( J |`t U ) Cn ( J |`t U ) ) )