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 25598
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 25597 . 2  class  TopFld
2 vg . . . . . . 7  set  g
32cv 1622 . . . . . 6  class  g
4 vh . . . . . . 7  set  h
54cv 1622 . . . . . 6  class  h
63, 5cop 3643 . . . . 5  class  <. g ,  h >.
7 cfld 21080 . . . . 5  class  Fld
86, 7wcel 1684 . . . 4  wff  <. g ,  h >.  e.  Fld
9 vj . . . . . . 7  set  j
109cv 1622 . . . . . 6  class  j
116, 10cop 3643 . . . . 5  class  <. <. g ,  h >. ,  j >.
12 ctrg 17838 . . . . 5  class  TopRing
1311, 12wcel 1684 . . . 4  wff  <. <. g ,  h >. ,  j >.  e.  TopRing
143crn 4690 . . . . . . . 8  class  ran  g
15 cgi 20854 . . . . . . . . . 10  class GId
163, 15cfv 5255 . . . . . . . . 9  class  (GId `  g )
1716csn 3640 . . . . . . . 8  class  { (GId
`  g ) }
1814, 17cdif 3149 . . . . . . 7  class  ( ran  g  \  { (GId
`  g ) } )
1918, 18cxp 4687 . . . . . 6  class  ( ( ran  g  \  {
(GId `  g ) } )  X.  ( ran  g  \  { (GId
`  g ) } ) )
205, 19cres 4691 . . . . 5  class  ( h  |`  ( ( ran  g  \  { (GId `  g
) } )  X.  ( ran  g  \  { (GId `  g ) } ) ) )
21 ctx 17255 . . . . . . 7  class  tX
2210, 10, 21co 5858 . . . . . 6  class  ( j 
tX  j )
23 ccn 16954 . . . . . 6  class  Cn
2422, 10, 23co 5858 . . . . 5  class  ( ( j  tX  j )  Cn  j )
2520, 24wcel 1684 . . . 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 5859 . 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 1623 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