Definition df-trg

Description: Define a topological ring, which is a ring such that the addition is a topological group operation and the multiplication is continuous. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Assertion	df-trg	|- TopRing = { r e. ( TopGrp i^i Ring ) | ( mulGrp ` r ) e. TopMnd }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctrg	|- TopRing
1		vr	|- r
2		ctgp	|- TopGrp
3		crg	|- Ring
4	2 3	cin	|- ( TopGrp i^i Ring )
5		cmgp	|- mulGrp
6	1	cv	|- r
7	6 5	cfv	|- ( mulGrp ` r )
8		ctmd	|- TopMnd
9	7 8	wcel	|- ( mulGrp ` r ) e. TopMnd
10	9 1 4	crab	|- { r e. ( TopGrp i^i Ring ) | ( mulGrp ` r ) e. TopMnd }
11	0 10	wceq	|- TopRing = { r e. ( TopGrp i^i Ring ) | ( mulGrp ` r ) e. TopMnd }