Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-edring-rN Unicode version

Definition df-edring-rN 30213
Description: Define division ring on trace-preserving endomorphisms. Definition of E of [Crawley] p. 117, 4th line from bottom. (Contributed by NM, 8-Jun-2013.)
Assertion
Ref Expression
df-edring-rN  |-  EDRing R  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  {
<. ( Base `  ndx ) ,  ( ( TEndo `  k ) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  t  e.  (
( TEndo `  k ) `  w )  |->  ( f  e.  ( ( LTrn `  k ) `  w
)  |->  ( ( s `
 f )  o.  ( t `  f
) ) ) )
>. ,  <. ( .r
`  ndx ) ,  ( s  e.  ( (
TEndo `  k ) `  w ) ,  t  e.  ( ( TEndo `  k ) `  w
)  |->  ( t  o.  s ) ) >. } ) )
Distinct variable group:    w, k, f, s, t

Detailed syntax breakdown of Definition df-edring-rN
StepHypRef Expression
1 cedring-rN 30211 . 2  class  EDRing R
2 vk . . 3  set  k
3 cvv 2790 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1623 . . . . 5  class  k
6 clh 29441 . . . . 5  class  LHyp
75, 6cfv 5222 . . . 4  class  ( LHyp `  k )
8 cnx 13140 . . . . . . 7  class  ndx
9 cbs 13143 . . . . . . 7  class  Base
108, 9cfv 5222 . . . . . 6  class  ( Base `  ndx )
114cv 1623 . . . . . . 7  class  w
12 ctendo 30209 . . . . . . . 8  class  TEndo
135, 12cfv 5222 . . . . . . 7  class  ( TEndo `  k )
1411, 13cfv 5222 . . . . . 6  class  ( (
TEndo `  k ) `  w )
1510, 14cop 3645 . . . . 5  class  <. ( Base `  ndx ) ,  ( ( TEndo `  k
) `  w ) >.
16 cplusg 13203 . . . . . . 7  class  +g
178, 16cfv 5222 . . . . . 6  class  ( +g  ` 
ndx )
18 vs . . . . . . 7  set  s
19 vt . . . . . . 7  set  t
20 vf . . . . . . . 8  set  f
21 cltrn 29558 . . . . . . . . . 10  class  LTrn
225, 21cfv 5222 . . . . . . . . 9  class  ( LTrn `  k )
2311, 22cfv 5222 . . . . . . . 8  class  ( (
LTrn `  k ) `  w )
2420cv 1623 . . . . . . . . . 10  class  f
2518cv 1623 . . . . . . . . . 10  class  s
2624, 25cfv 5222 . . . . . . . . 9  class  ( s `
 f )
2719cv 1623 . . . . . . . . . 10  class  t
2824, 27cfv 5222 . . . . . . . . 9  class  ( t `
 f )
2926, 28ccom 4693 . . . . . . . 8  class  ( ( s `  f )  o.  ( t `  f ) )
3020, 23, 29cmpt 4079 . . . . . . 7  class  ( f  e.  ( ( LTrn `  k ) `  w
)  |->  ( ( s `
 f )  o.  ( t `  f
) ) )
3118, 19, 14, 14, 30cmpt2 5822 . . . . . 6  class  ( s  e.  ( ( TEndo `  k ) `  w
) ,  t  e.  ( ( TEndo `  k
) `  w )  |->  ( f  e.  ( ( LTrn `  k
) `  w )  |->  ( ( s `  f )  o.  (
t `  f )
) ) )
3217, 31cop 3645 . . . . 5  class  <. ( +g  `  ndx ) ,  ( s  e.  ( ( TEndo `  k ) `  w ) ,  t  e.  ( ( TEndo `  k ) `  w
)  |->  ( f  e.  ( ( LTrn `  k
) `  w )  |->  ( ( s `  f )  o.  (
t `  f )
) ) ) >.
33 cmulr 13204 . . . . . . 7  class  .r
348, 33cfv 5222 . . . . . 6  class  ( .r
`  ndx )
3527, 25ccom 4693 . . . . . . 7  class  ( t  o.  s )
3618, 19, 14, 14, 35cmpt2 5822 . . . . . 6  class  ( s  e.  ( ( TEndo `  k ) `  w
) ,  t  e.  ( ( TEndo `  k
) `  w )  |->  ( t  o.  s
) )
3734, 36cop 3645 . . . . 5  class  <. ( .r `  ndx ) ,  ( s  e.  ( ( TEndo `  k ) `  w ) ,  t  e.  ( ( TEndo `  k ) `  w
)  |->  ( t  o.  s ) ) >.
3815, 32, 37ctp 3644 . . . 4  class  { <. (
Base `  ndx ) ,  ( ( TEndo `  k
) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  t  e.  (
( TEndo `  k ) `  w )  |->  ( f  e.  ( ( LTrn `  k ) `  w
)  |->  ( ( s `
 f )  o.  ( t `  f
) ) ) )
>. ,  <. ( .r
`  ndx ) ,  ( s  e.  ( (
TEndo `  k ) `  w ) ,  t  e.  ( ( TEndo `  k ) `  w
)  |->  ( t  o.  s ) ) >. }
394, 7, 38cmpt 4079 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  { <. ( Base `  ndx ) ,  ( ( TEndo `  k
) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  t  e.  (
( TEndo `  k ) `  w )  |->  ( f  e.  ( ( LTrn `  k ) `  w
)  |->  ( ( s `
 f )  o.  ( t `  f
) ) ) )
>. ,  <. ( .r
`  ndx ) ,  ( s  e.  ( (
TEndo `  k ) `  w ) ,  t  e.  ( ( TEndo `  k ) `  w
)  |->  ( t  o.  s ) ) >. } )
402, 3, 39cmpt 4079 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  { <. ( Base `  ndx ) ,  ( ( TEndo `  k
) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  t  e.  (
( TEndo `  k ) `  w )  |->  ( f  e.  ( ( LTrn `  k ) `  w
)  |->  ( ( s `
 f )  o.  ( t `  f
) ) ) )
>. ,  <. ( .r
`  ndx ) ,  ( s  e.  ( (
TEndo `  k ) `  w ) ,  t  e.  ( ( TEndo `  k ) `  w
)  |->  ( t  o.  s ) ) >. } ) )
411, 40wceq 1624 1  wff  EDRing R  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  {
<. ( Base `  ndx ) ,  ( ( TEndo `  k ) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  t  e.  (
( TEndo `  k ) `  w )  |->  ( f  e.  ( ( LTrn `  k ) `  w
)  |->  ( ( s `
 f )  o.  ( t `  f
) ) ) )
>. ,  <. ( .r
`  ndx ) ,  ( s  e.  ( (
TEndo `  k ) `  w ) ,  t  e.  ( ( TEndo `  k ) `  w
)  |->  ( t  o.  s ) ) >. } ) )
Colors of variables: wff set class
This definition is referenced by:  erngfset-rN  30264
  Copyright terms: Public domain W3C validator