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 = { 𝑟 ∈ ( TopGrp ∩ Ring ) ∣ ( mulGrp ‘ 𝑟 ) ∈ TopMnd }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctrg	⊢ TopRing
1		vr	⊢ 𝑟
2		ctgp	⊢ TopGrp
3		crg	⊢ Ring
4	2 3	cin	⊢ ( TopGrp ∩ Ring )
5		cmgp	⊢ mulGrp
6	1	cv	⊢ 𝑟
7	6 5	cfv	⊢ ( mulGrp ‘ 𝑟 )
8		ctmd	⊢ TopMnd
9	7 8	wcel	⊢ ( mulGrp ‘ 𝑟 ) ∈ TopMnd
10	9 1 4	crab	⊢ { 𝑟 ∈ ( TopGrp ∩ Ring ) ∣ ( mulGrp ‘ 𝑟 ) ∈ TopMnd }
11	0 10	wceq	⊢ TopRing = { 𝑟 ∈ ( TopGrp ∩ Ring ) ∣ ( mulGrp ‘ 𝑟 ) ∈ TopMnd }