This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in (TopGrp \cap Ring) \| {mulGrp}_{r} \in TopMnd\}$

Detailed syntax breakdown

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