Metamath Proof Explorer

Definition df-edring

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)

Ref Expression
Assertion 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 ) ) >. } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cedring 
 |-  EDRing
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 23 26 ccom 
 |-  ( s o. t )
35 17 18 13 13 34 cmpo 
 |-  ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( s o. t ) )
36 33 35 cop 
 |-  <. ( .r ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( s o. t ) ) >.
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 ) |-> ( s o. t ) ) >. }
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 ) |-> ( s o. t ) ) >. } )
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 ) |-> ( s o. t ) ) >. } ) )
40 0 39 wceq 
 |-  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 ) ) >. } ) )