Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-topfld Unicode version

Definition df-topfld 25701
Description: A topological field is a field whose addition, multiplication and inverse are continuous. (Contributed by FL, 21-May-2012.)
Assertion
Ref Expression
df-topfld  |-  TopFld  =  { <. <. g ,  h >. ,  j >.  |  (
<. g ,  h >.  e. 
Fld  /\  <. <. g ,  h >. ,  j >.  e.  TopRing  /\  ( h  |`  ( ( ran  g  \  { (GId `  g
) } )  X.  ( ran  g  \  { (GId `  g ) } ) ) )  e.  ( ( j 
tX  j )  Cn  j ) ) }
Distinct variable group:    g, h, j

Detailed syntax breakdown of Definition df-topfld
StepHypRef Expression
1 ctopfld 25700 . 2  class  TopFld
2 vg . . . . . . 7  set  g
32cv 1631 . . . . . 6  class  g
4 vh . . . . . . 7  set  h
54cv 1631 . . . . . 6  class  h
63, 5cop 3656 . . . . 5  class  <. g ,  h >.
7 cfld 21096 . . . . 5  class  Fld
86, 7wcel 1696 . . . 4  wff  <. g ,  h >.  e.  Fld
9 vj . . . . . . 7  set  j
109cv 1631 . . . . . 6  class  j
116, 10cop 3656 . . . . 5  class  <. <. g ,  h >. ,  j >.
12 ctrg 17854 . . . . 5  class  TopRing
1311, 12wcel 1696 . . . 4  wff  <. <. g ,  h >. ,  j >.  e.  TopRing
143crn 4706 . . . . . . . 8  class  ran  g
15 cgi 20870 . . . . . . . . . 10  class GId
163, 15cfv 5271 . . . . . . . . 9  class  (GId `  g )
1716csn 3653 . . . . . . . 8  class  { (GId
`  g ) }
1814, 17cdif 3162 . . . . . . 7  class  ( ran  g  \  { (GId
`  g ) } )
1918, 18cxp 4703 . . . . . 6  class  ( ( ran  g  \  {
(GId `  g ) } )  X.  ( ran  g  \  { (GId
`  g ) } ) )
205, 19cres 4707 . . . . 5  class  ( h  |`  ( ( ran  g  \  { (GId `  g
) } )  X.  ( ran  g  \  { (GId `  g ) } ) ) )
21 ctx 17271 . . . . . . 7  class  tX
2210, 10, 21co 5874 . . . . . 6  class  ( j 
tX  j )
23 ccn 16970 . . . . . 6  class  Cn
2422, 10, 23co 5874 . . . . 5  class  ( ( j  tX  j )  Cn  j )
2520, 24wcel 1696 . . . 4  wff  ( h  |`  ( ( ran  g  \  { (GId `  g
) } )  X.  ( ran  g  \  { (GId `  g ) } ) ) )  e.  ( ( j 
tX  j )  Cn  j )
268, 13, 25w3a 934 . . 3  wff  ( <.
g ,  h >.  e. 
Fld  /\  <. <. g ,  h >. ,  j >.  e.  TopRing  /\  ( h  |`  ( ( ran  g  \  { (GId `  g
) } )  X.  ( ran  g  \  { (GId `  g ) } ) ) )  e.  ( ( j 
tX  j )  Cn  j ) )
2726, 2, 4, 9coprab 5875 . 2  class  { <. <.
g ,  h >. ,  j >.  |  ( <. g ,  h >.  e. 
Fld  /\  <. <. g ,  h >. ,  j >.  e.  TopRing  /\  ( h  |`  ( ( ran  g  \  { (GId `  g
) } )  X.  ( ran  g  \  { (GId `  g ) } ) ) )  e.  ( ( j 
tX  j )  Cn  j ) ) }
281, 27wceq 1632 1  wff  TopFld  =  { <. <. g ,  h >. ,  j >.  |  (
<. g ,  h >.  e. 
Fld  /\  <. <. g ,  h >. ,  j >.  e.  TopRing  /\  ( h  |`  ( ( ran  g  \  { (GId `  g
) } )  X.  ( ran  g  \  { (GId `  g ) } ) ) )  e.  ( ( j 
tX  j )  Cn  j ) ) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator