Metamath Proof Explorer

Definition df-mend

Description: Define the endomorphism algebra of a module. (Contributed by Stefan O'Rear, 2-Sep-2015)

Ref Expression
Assertion df-mend 
|- MEndo = ( m e. _V |-> [_ ( m LMHom m ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmend 
 |-  MEndo
1 vm 
 |-  m
2 cvv 
 |-  _V
3 1 cv 
 |-  m
4 clmhm 
 |-  LMHom
5 3 3 4 co 
 |-  ( m LMHom m )
6 vb 
 |-  b
7 cbs 
 |-  Base
8 cnx 
 |-  ndx
9 8 7 cfv 
 |-  ( Base ` ndx )
10 6 cv 
 |-  b
11 9 10 cop 
 |-  <. ( Base ` ndx ) , b >.
12 cplusg 
 |-  +g
13 8 12 cfv 
 |-  ( +g ` ndx )
14 vx 
 |-  x
15 vy 
 |-  y
16 14 cv 
 |-  x
17 3 12 cfv 
 |-  ( +g ` m )
18 17 cof 
 |-  oF ( +g ` m )
19 15 cv 
 |-  y
20 16 19 18 co 
 |-  ( x oF ( +g ` m ) y )
21 14 15 10 10 20 cmpo 
 |-  ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) )
22 13 21 cop 
 |-  <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >.
23 cmulr 
 |-  .r
24 8 23 cfv 
 |-  ( .r ` ndx )
25 16 19 ccom 
 |-  ( x o. y )
26 14 15 10 10 25 cmpo 
 |-  ( x e. b , y e. b |-> ( x o. y ) )
27 24 26 cop 
 |-  <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >.
28 11 22 27 ctp 
 |-  { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. }
29 csca 
 |-  Scalar
30 8 29 cfv 
 |-  ( Scalar ` ndx )
31 3 29 cfv 
 |-  ( Scalar ` m )
32 30 31 cop 
 |-  <. ( Scalar ` ndx ) , ( Scalar ` m ) >.
33 cvsca 
 |-  .s
34 8 33 cfv 
 |-  ( .s ` ndx )
35 31 7 cfv 
 |-  ( Base ` ( Scalar ` m ) )
36 3 7 cfv 
 |-  ( Base ` m )
37 16 csn 
 |-  { x }
38 36 37 cxp 
 |-  ( ( Base ` m ) X. { x } )
39 3 33 cfv 
 |-  ( .s ` m )
40 39 cof 
 |-  oF ( .s ` m )
41 38 19 40 co 
 |-  ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y )
42 14 15 35 10 41 cmpo 
 |-  ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) )
43 34 42 cop 
 |-  <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >.
44 32 43 cpr 
 |-  { <. ( Scalar ` ndx ) , ( Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. }
45 28 44 cun 
 |-  ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } )
46 6 5 45 csb 
 |-  [_ ( m LMHom m ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } )
47 1 2 46 cmpt 
 |-  ( m e. _V |-> [_ ( m LMHom m ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } ) )
48 0 47 wceq 
 |-  MEndo = ( m e. _V |-> [_ ( m LMHom m ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } ) )