MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-trg Unicode version

Definition df-trg 17842
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.)
Assertion
Ref Expression
df-trg  |-  TopRing  =  {
r  e.  ( TopGrp  i^i 
Ring )  |  (mulGrp `  r )  e. TopMnd }

Detailed syntax breakdown of Definition df-trg
StepHypRef Expression
1 ctrg 17838 . 2  class  TopRing
2 vr . . . . . 6  set  r
32cv 1622 . . . . 5  class  r
4 cmgp 15325 . . . . 5  class mulGrp
53, 4cfv 5255 . . . 4  class  (mulGrp `  r )
6 ctmd 17753 . . . 4  class TopMnd
75, 6wcel 1684 . . 3  wff  (mulGrp `  r )  e. TopMnd
8 ctgp 17754 . . . 4  class  TopGrp
9 crg 15337 . . . 4  class  Ring
108, 9cin 3151 . . 3  class  ( TopGrp  i^i 
Ring )
117, 2, 10crab 2547 . 2  class  { r  e.  ( TopGrp  i^i  Ring )  |  (mulGrp `  r
)  e. TopMnd }
121, 11wceq 1623 1  wff  TopRing  =  {
r  e.  ( TopGrp  i^i 
Ring )  |  (mulGrp `  r )  e. TopMnd }
Colors of variables: wff set class
This definition is referenced by:  istrg  17846
  Copyright terms: Public domain W3C validator