Metamath Proof Explorer


Definition df-edring-rN

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)

Ref Expression
Assertion df-edring-rN
|- EDRingR = ( 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 ) ) >. } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cedring-rN
 |-  EDRingR
1 vk
 |-  k
2 cvv
 |-  _V
3 vw
 |-  w
4 clh
 |-  LHyp
5 1 cv
 |-  k
6 5 4 cfv
 |-  ( LHyp ` k )
7 cbs
 |-  Base
8 cnx
 |-  ndx
9 8 7 cfv
 |-  ( Base ` ndx )
10 ctendo
 |-  TEndo
11 5 10 cfv
 |-  ( TEndo ` k )
12 3 cv
 |-  w
13 12 11 cfv
 |-  ( ( TEndo ` k ) ` w )
14 9 13 cop
 |-  <. ( Base ` ndx ) , ( ( TEndo ` k ) ` w ) >.
15 cplusg
 |-  +g
16 8 15 cfv
 |-  ( +g ` ndx )
17 vs
 |-  s
18 vt
 |-  t
19 vf
 |-  f
20 cltrn
 |-  LTrn
21 5 20 cfv
 |-  ( LTrn ` k )
22 12 21 cfv
 |-  ( ( LTrn ` k ) ` w )
23 17 cv
 |-  s
24 19 cv
 |-  f
25 24 23 cfv
 |-  ( s ` f )
26 18 cv
 |-  t
27 24 26 cfv
 |-  ( t ` f )
28 25 27 ccom
 |-  ( ( s ` f ) o. ( t ` f ) )
29 19 22 28 cmpt
 |-  ( f e. ( ( LTrn ` k ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) )
30 17 18 13 13 29 cmpo
 |-  ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( f e. ( ( LTrn ` k ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) )
31 16 30 cop
 |-  <. ( +g ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( f e. ( ( LTrn ` k ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >.
32 cmulr
 |-  .r
33 8 32 cfv
 |-  ( .r ` ndx )
34 26 23 ccom
 |-  ( t o. s )
35 17 18 13 13 34 cmpo
 |-  ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( t o. s ) )
36 33 35 cop
 |-  <. ( .r ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( t o. s ) ) >.
37 14 31 36 ctp
 |-  { <. ( 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 ) ) >. }
38 3 6 37 cmpt
 |-  ( 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 ) ) >. } )
39 1 2 38 cmpt
 |-  ( 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 ) ) >. } ) )
40 0 39 wceq
 |-  EDRingR = ( 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 ) ) >. } ) )