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

Definition df-edring 30946
Description: Define division ring on trace-preserving endomorphisms. The multiplication operation is reversed composition, per the definition of E of [Crawley] p. 117, 4th line from bottom. (Contributed by NM, 8-Jun-2013.)
Assertion
Ref Expression
df-edring  |-  EDRing  =  ( 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
)  |->  ( s  o.  t ) ) >. } ) )
Distinct variable group:    w, k, f, s, t

Detailed syntax breakdown of Definition df-edring
StepHypRef Expression
1 cedring 30942 . 2  class  EDRing
2 vk . . 3  set  k
3 cvv 2788 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1622 . . . . 5  class  k
6 clh 30173 . . . . 5  class  LHyp
75, 6cfv 5255 . . . 4  class  ( LHyp `  k )
8 cnx 13145 . . . . . . 7  class  ndx
9 cbs 13148 . . . . . . 7  class  Base
108, 9cfv 5255 . . . . . 6  class  ( Base `  ndx )
114cv 1622 . . . . . . 7  class  w
12 ctendo 30941 . . . . . . . 8  class  TEndo
135, 12cfv 5255 . . . . . . 7  class  ( TEndo `  k )
1411, 13cfv 5255 . . . . . 6  class  ( (
TEndo `  k ) `  w )
1510, 14cop 3643 . . . . 5  class  <. ( Base `  ndx ) ,  ( ( TEndo `  k
) `  w ) >.
16 cplusg 13208 . . . . . . 7  class  +g
178, 16cfv 5255 . . . . . 6  class  ( +g  ` 
ndx )
18 vs . . . . . . 7  set  s
19 vt . . . . . . 7  set  t
20 vf . . . . . . . 8  set  f
21 cltrn 30290 . . . . . . . . . 10  class  LTrn
225, 21cfv 5255 . . . . . . . . 9  class  ( LTrn `  k )
2311, 22cfv 5255 . . . . . . . 8  class  ( (
LTrn `  k ) `  w )
2420cv 1622 . . . . . . . . . 10  class  f
2518cv 1622 . . . . . . . . . 10  class  s
2624, 25cfv 5255 . . . . . . . . 9  class  ( s `
 f )
2719cv 1622 . . . . . . . . . 10  class  t
2824, 27cfv 5255 . . . . . . . . 9  class  ( t `
 f )
2926, 28ccom 4693 . . . . . . . 8  class  ( ( s `  f )  o.  ( t `  f ) )
3020, 23, 29cmpt 4077 . . . . . . 7  class  ( f  e.  ( ( LTrn `  k ) `  w
)  |->  ( ( s `
 f )  o.  ( t `  f
) ) )
3118, 19, 14, 14, 30cmpt2 5860 . . . . . 6  class  ( s  e.  ( ( TEndo `  k ) `  w
) ,  t  e.  ( ( TEndo `  k
) `  w )  |->  ( f  e.  ( ( LTrn `  k
) `  w )  |->  ( ( s `  f )  o.  (
t `  f )
) ) )
3217, 31cop 3643 . . . . 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 13209 . . . . . . 7  class  .r
348, 33cfv 5255 . . . . . 6  class  ( .r
`  ndx )
3525, 27ccom 4693 . . . . . . 7  class  ( s  o.  t )
3618, 19, 14, 14, 35cmpt2 5860 . . . . . 6  class  ( s  e.  ( ( TEndo `  k ) `  w
) ,  t  e.  ( ( TEndo `  k
) `  w )  |->  ( s  o.  t
) )
3734, 36cop 3643 . . . . 5  class  <. ( .r `  ndx ) ,  ( s  e.  ( ( TEndo `  k ) `  w ) ,  t  e.  ( ( TEndo `  k ) `  w
)  |->  ( s  o.  t ) ) >.
3815, 32, 37ctp 3642 . . . 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
)  |->  ( s  o.  t ) ) >. }
394, 7, 38cmpt 4077 . . 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
)  |->  ( s  o.  t ) ) >. } )
402, 3, 39cmpt 4077 . 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
)  |->  ( s  o.  t ) ) >. } ) )
411, 40wceq 1623 1  wff  EDRing  =  ( 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
)  |->  ( s  o.  t ) ) >. } ) )
Colors of variables: wff set class
This definition is referenced by:  erngfset  30988
  Copyright terms: Public domain W3C validator