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	$$⊢\mathrm{TopRing}=\left\{r\in \left(\mathrm{TopGrp}\cap \mathrm{Ring}\right)|{\mathrm{mulGrp}}_r\in \mathrm{TopMnd}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctrg	$$class\mathrm{TopRing}$$
1		vr	$$setvarr$$
2		ctgp	$$class\mathrm{TopGrp}$$
3		crg	$$class\mathrm{Ring}$$
4	2 3	cin	$$class\left(\mathrm{TopGrp}\cap \mathrm{Ring}\right)$$
5		cmgp	$$class\mathrm{mulGrp}$$
6	1	cv	$$setvarr$$
7	6 5	cfv	$$class{\mathrm{mulGrp}}_r$$
8		ctmd	$$class\mathrm{TopMnd}$$
9	7 8	wcel	$$wff{\mathrm{mulGrp}}_r\in \mathrm{TopMnd}$$
10	9 1 4	crab	$$class\left\{r\in \left(\mathrm{TopGrp}\cap \mathrm{Ring}\right)|{\mathrm{mulGrp}}_r\in \mathrm{TopMnd}\right\}$$
11	0 10	wceq	$$wff\mathrm{TopRing}=\left\{r\in \left(\mathrm{TopGrp}\cap \mathrm{Ring}\right)|{\mathrm{mulGrp}}_r\in \mathrm{TopMnd}\right\}$$