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

Definition df-sfld 21076
Description: Define the class of all star fields, which are all division rings with involutions. (Contributed by NM, 29-Aug-2010.) (New usage is discouraged.)
Assertion
Ref Expression
df-sfld  |-  *-Fld  =  { <. r ,  n >.  |  ( r  e.  DivRingOps  /\  n : ran  ( 1st `  r
) --> ran  ( 1st `  r )  /\  A. x  e.  dom  n A. y  e.  dom  n ( ( n `  (
x ( 1st `  r
) y ) )  =  ( ( n `
 x ) ( 1st `  r ) ( n `  y
) )  /\  (
n `  ( x
( 2nd `  r
) y ) )  =  ( ( n `
 y ) ( 2nd `  r ) ( n `  x
) )  /\  (
n `  ( n `  x ) )  =  x ) ) }
Distinct variable group:    n, r, x, y

Detailed syntax breakdown of Definition df-sfld
StepHypRef Expression
1 csfld 21075 . 2  class  *-Fld
2 vr . . . . . 6  set  r
32cv 1622 . . . . 5  class  r
4 cdrng 21072 . . . . 5  class  DivRingOps
53, 4wcel 1684 . . . 4  wff  r  e.  DivRingOps
6 c1st 6120 . . . . . . 7  class  1st
73, 6cfv 5255 . . . . . 6  class  ( 1st `  r )
87crn 4690 . . . . 5  class  ran  ( 1st `  r )
9 vn . . . . . 6  set  n
109cv 1622 . . . . 5  class  n
118, 8, 10wf 5251 . . . 4  wff  n : ran  ( 1st `  r
) --> ran  ( 1st `  r )
12 vx . . . . . . . . . . 11  set  x
1312cv 1622 . . . . . . . . . 10  class  x
14 vy . . . . . . . . . . 11  set  y
1514cv 1622 . . . . . . . . . 10  class  y
1613, 15, 7co 5858 . . . . . . . . 9  class  ( x ( 1st `  r
) y )
1716, 10cfv 5255 . . . . . . . 8  class  ( n `
 ( x ( 1st `  r ) y ) )
1813, 10cfv 5255 . . . . . . . . 9  class  ( n `
 x )
1915, 10cfv 5255 . . . . . . . . 9  class  ( n `
 y )
2018, 19, 7co 5858 . . . . . . . 8  class  ( ( n `  x ) ( 1st `  r
) ( n `  y ) )
2117, 20wceq 1623 . . . . . . 7  wff  ( n `
 ( x ( 1st `  r ) y ) )  =  ( ( n `  x ) ( 1st `  r ) ( n `
 y ) )
22 c2nd 6121 . . . . . . . . . . 11  class  2nd
233, 22cfv 5255 . . . . . . . . . 10  class  ( 2nd `  r )
2413, 15, 23co 5858 . . . . . . . . 9  class  ( x ( 2nd `  r
) y )
2524, 10cfv 5255 . . . . . . . 8  class  ( n `
 ( x ( 2nd `  r ) y ) )
2619, 18, 23co 5858 . . . . . . . 8  class  ( ( n `  y ) ( 2nd `  r
) ( n `  x ) )
2725, 26wceq 1623 . . . . . . 7  wff  ( n `
 ( x ( 2nd `  r ) y ) )  =  ( ( n `  y ) ( 2nd `  r ) ( n `
 x ) )
2818, 10cfv 5255 . . . . . . . 8  class  ( n `
 ( n `  x ) )
2928, 13wceq 1623 . . . . . . 7  wff  ( n `
 ( n `  x ) )  =  x
3021, 27, 29w3a 934 . . . . . 6  wff  ( ( n `  ( x ( 1st `  r
) y ) )  =  ( ( n `
 x ) ( 1st `  r ) ( n `  y
) )  /\  (
n `  ( x
( 2nd `  r
) y ) )  =  ( ( n `
 y ) ( 2nd `  r ) ( n `  x
) )  /\  (
n `  ( n `  x ) )  =  x )
3110cdm 4689 . . . . . 6  class  dom  n
3230, 14, 31wral 2543 . . . . 5  wff  A. y  e.  dom  n ( ( n `  ( x ( 1st `  r
) y ) )  =  ( ( n `
 x ) ( 1st `  r ) ( n `  y
) )  /\  (
n `  ( x
( 2nd `  r
) y ) )  =  ( ( n `
 y ) ( 2nd `  r ) ( n `  x
) )  /\  (
n `  ( n `  x ) )  =  x )
3332, 12, 31wral 2543 . . . 4  wff  A. x  e.  dom  n A. y  e.  dom  n ( ( n `  ( x ( 1st `  r
) y ) )  =  ( ( n `
 x ) ( 1st `  r ) ( n `  y
) )  /\  (
n `  ( x
( 2nd `  r
) y ) )  =  ( ( n `
 y ) ( 2nd `  r ) ( n `  x
) )  /\  (
n `  ( n `  x ) )  =  x )
345, 11, 33w3a 934 . . 3  wff  ( r  e.  DivRingOps  /\  n : ran  ( 1st `  r ) --> ran  ( 1st `  r
)  /\  A. x  e.  dom  n A. y  e.  dom  n ( ( n `  ( x ( 1st `  r
) y ) )  =  ( ( n `
 x ) ( 1st `  r ) ( n `  y
) )  /\  (
n `  ( x
( 2nd `  r
) y ) )  =  ( ( n `
 y ) ( 2nd `  r ) ( n `  x
) )  /\  (
n `  ( n `  x ) )  =  x ) )
3534, 2, 9copab 4076 . 2  class  { <. r ,  n >.  |  ( r  e.  DivRingOps  /\  n : ran  ( 1st `  r
) --> ran  ( 1st `  r )  /\  A. x  e.  dom  n A. y  e.  dom  n ( ( n `  (
x ( 1st `  r
) y ) )  =  ( ( n `
 x ) ( 1st `  r ) ( n `  y
) )  /\  (
n `  ( x
( 2nd `  r
) y ) )  =  ( ( n `
 y ) ( 2nd `  r ) ( n `  x
) )  /\  (
n `  ( n `  x ) )  =  x ) ) }
361, 35wceq 1623 1  wff  *-Fld  =  { <. r ,  n >.  |  ( r  e.  DivRingOps  /\  n : ran  ( 1st `  r
) --> ran  ( 1st `  r )  /\  A. x  e.  dom  n A. y  e.  dom  n ( ( n `  (
x ( 1st `  r
) y ) )  =  ( ( n `
 x ) ( 1st `  r ) ( n `  y
) )  /\  (
n `  ( x
( 2nd `  r
) y ) )  =  ( ( n `
 y ) ( 2nd `  r ) ( n `  x
) )  /\  (
n `  ( n `  x ) )  =  x ) ) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator