Theorem mgptopn

Description: Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	mgpbas.1	|- M = ( mulGrp ` R )
	mgptopn.2	|- J = ( TopOpen ` R )
Assertion	mgptopn	|- J = ( TopOpen ` M )

Proof

Step	Hyp	Ref	Expression
1		mgpbas.1	|- M = ( mulGrp ` R )
2		mgptopn.2	|- J = ( TopOpen ` R )
3		eqid	|- ( Base ` R ) = ( Base ` R )
4		eqid	|- ( TopSet ` R ) = ( TopSet ` R )
5	3 4	topnval	|- ( ( TopSet ` R ) |`t ( Base ` R ) ) = ( TopOpen ` R )
6	1 3	mgpbas	|- ( Base ` R ) = ( Base ` M )
7	1	mgptset	|- ( TopSet ` R ) = ( TopSet ` M )
8	6 7	topnval	|- ( ( TopSet ` R ) |`t ( Base ` R ) ) = ( TopOpen ` M )
9	2 5 8	3eqtr2i	|- J = ( TopOpen ` M )