Metamath Proof Explorer

Theorem mendvscafval

Description: Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015) (Proof shortened by AV, 3-Mar-2024)

Ref Expression
Hypotheses mendvscafval.a 
|- A = ( MEndo ` M )
mendvscafval.v 
|- .x. = ( .s ` M )
mendvscafval.b 
|- B = ( Base ` A )
mendvscafval.s 
|- S = ( Scalar ` M )
mendvscafval.k 
|- K = ( Base ` S )
mendvscafval.e 
|- E = ( Base ` M )
Assertion mendvscafval 
|- ( .s ` A ) = ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) )

Proof

Step Hyp Ref Expression
1 mendvscafval.a 
 |-  A = ( MEndo ` M )
2 mendvscafval.v 
 |-  .x. = ( .s ` M )
3 mendvscafval.b 
 |-  B = ( Base ` A )
4 mendvscafval.s 
 |-  S = ( Scalar ` M )
5 mendvscafval.k 
 |-  K = ( Base ` S )
6 mendvscafval.e 
 |-  E = ( Base ` M )
7 1 fveq2i 
 |-  ( .s ` A ) = ( .s ` ( MEndo ` M ) )
8 1 mendbas 
 |-  ( M LMHom M ) = ( Base ` A )
9 3 8 eqtr4i 
 |-  B = ( M LMHom M )
10 eqid 
 |-  ( x e. B , y e. B |-> ( x oF ( +g ` M ) y ) ) = ( x e. B , y e. B |-> ( x oF ( +g ` M ) y ) )
11 eqid 
 |-  ( x e. B , y e. B |-> ( x o. y ) ) = ( x e. B , y e. B |-> ( x o. y ) )
12 eqid 
 |-  B = B
13 6 xpeq1i 
 |-  ( E X. { x } ) = ( ( Base ` M ) X. { x } )
14 eqid 
 |-  y = y
15 ofeq 
 |-  ( .x. = ( .s ` M ) -> oF .x. = oF ( .s ` M ) )
16 2 15 ax-mp 
 |-  oF .x. = oF ( .s ` M )
17 13 14 16 oveq123i 
 |-  ( ( E X. { x } ) oF .x. y ) = ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y )
18 5 12 17 mpoeq123i 
 |-  ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) ) = ( x e. ( Base ` S ) , y e. B |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) )
19 9 10 11 4 18 mendval 
 |-  ( M e. _V -> ( MEndo ` M ) = ( { <. ( 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 ) , S >. , <. ( .s ` ndx ) , ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) ) >. } ) )
20 19 fveq2d 
 |-  ( M e. _V -> ( .s ` ( MEndo ` M ) ) = ( .s ` ( { <. ( 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 ) , S >. , <. ( .s ` ndx ) , ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) ) >. } ) ) )
21 5 fvexi 
 |-  K e. _V
22 3 fvexi 
 |-  B e. _V
23 21 22 mpoex 
 |-  ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) ) e. _V
24 eqid 
 |-  ( { <. ( 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 ) , S >. , <. ( .s ` ndx ) , ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) ) >. } ) = ( { <. ( 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 ) , S >. , <. ( .s ` ndx ) , ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) ) >. } )
25 24 algvsca 
 |-  ( ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) ) e. _V -> ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) ) = ( .s ` ( { <. ( 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 ) , S >. , <. ( .s ` ndx ) , ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) ) >. } ) ) )
26 23 25 mp1i 
 |-  ( M e. _V -> ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) ) = ( .s ` ( { <. ( 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 ) , S >. , <. ( .s ` ndx ) , ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) ) >. } ) ) )
27 20 26 eqtr4d 
 |-  ( M e. _V -> ( .s ` ( MEndo ` M ) ) = ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) ) )
28 fvprc 
 |-  ( -. M e. _V -> ( MEndo ` M ) = (/) )
29 28 fveq2d 
 |-  ( -. M e. _V -> ( .s ` ( MEndo ` M ) ) = ( .s ` (/) ) )
30 df-vsca 
 |-  .s = Slot 6
31 30 str0 
 |-  (/) = ( .s ` (/) )
32 29 31 eqtr4di 
 |-  ( -. M e. _V -> ( .s ` ( MEndo ` M ) ) = (/) )
33 fvprc 
 |-  ( -. M e. _V -> ( Scalar ` M ) = (/) )
34 4 33 syl5eq 
 |-  ( -. M e. _V -> S = (/) )
35 34 fveq2d 
 |-  ( -. M e. _V -> ( Base ` S ) = ( Base ` (/) ) )
36 base0 
 |-  (/) = ( Base ` (/) )
37 35 5 36 3eqtr4g 
 |-  ( -. M e. _V -> K = (/) )
38 37 orcd 
 |-  ( -. M e. _V -> ( K = (/) \/ B = (/) ) )
39 0mpo0 
 |-  ( ( K = (/) \/ B = (/) ) -> ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) ) = (/) )
40 38 39 syl 
 |-  ( -. M e. _V -> ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) ) = (/) )
41 32 40 eqtr4d 
 |-  ( -. M e. _V -> ( .s ` ( MEndo ` M ) ) = ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) ) )
42 27 41 pm2.61i 
 |-  ( .s ` ( MEndo ` M ) ) = ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) )
43 7 42 eqtri 
 |-  ( .s ` A ) = ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) )