Metamath Proof Explorer

Theorem mendmulrfval

Description: Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015) (Proof shortened by AV, 31-Oct-2024)

Ref Expression
Hypotheses mendmulrfval.a 
|- A = ( MEndo ` M )
mendmulrfval.b 
|- B = ( Base ` A )
Assertion mendmulrfval 
|- ( .r ` A ) = ( x e. B , y e. B |-> ( x o. y ) )

Proof

Step Hyp Ref Expression
1 mendmulrfval.a 
 |-  A = ( MEndo ` M )
2 mendmulrfval.b 
 |-  B = ( Base ` A )
3 1 mendbas 
 |-  ( M LMHom M ) = ( Base ` A )
4 2 3 eqtr4i 
 |-  B = ( M LMHom M )
5 eqid 
 |-  ( x e. B , y e. B |-> ( x oF ( +g ` M ) y ) ) = ( x e. B , y e. B |-> ( x oF ( +g ` M ) y ) )
6 eqid 
 |-  ( x e. B , y e. B |-> ( x o. y ) ) = ( x e. B , y e. B |-> ( x o. y ) )
7 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
8 eqid 
 |-  ( x e. ( Base ` ( Scalar ` M ) ) , y e. B |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) ) = ( x e. ( Base ` ( Scalar ` M ) ) , y e. B |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) )
9 4 5 6 7 8 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 ) , ( Scalar ` M ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` M ) ) , y e. B |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) ) >. } ) )
10 1 9 syl5eq 
 |-  ( M e. _V -> A = ( { <. ( 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 ) ) >. } ) )
11 10 fveq2d 
 |-  ( M e. _V -> ( .r ` A ) = ( .r ` ( { <. ( 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 ) ) >. } ) ) )
12 2 fvexi 
 |-  B e. _V
13 12 12 mpoex 
 |-  ( x e. B , y e. B |-> ( x o. y ) ) e. _V
14 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 ) , ( Scalar ` M ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` M ) ) , y e. B |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) 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 ) , ( Scalar ` M ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` M ) ) , y e. B |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) ) >. } )
15 14 algmulr 
 |-  ( ( x e. B , y e. B |-> ( x o. y ) ) e. _V -> ( x e. B , y e. B |-> ( x o. y ) ) = ( .r ` ( { <. ( 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 ) ) >. } ) ) )
16 13 15 mp1i 
 |-  ( M e. _V -> ( x e. B , y e. B |-> ( x o. y ) ) = ( .r ` ( { <. ( 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 ) ) >. } ) ) )
17 11 16 eqtr4d 
 |-  ( M e. _V -> ( .r ` A ) = ( x e. B , y e. B |-> ( x o. y ) ) )
18 fvprc 
 |-  ( -. M e. _V -> ( MEndo ` M ) = (/) )
19 1 18 syl5eq 
 |-  ( -. M e. _V -> A = (/) )
20 19 fveq2d 
 |-  ( -. M e. _V -> ( .r ` A ) = ( .r ` (/) ) )
21 mulrid 
 |-  .r = Slot ( .r ` ndx )
22 21 str0 
 |-  (/) = ( .r ` (/) )
23 20 22 eqtr4di 
 |-  ( -. M e. _V -> ( .r ` A ) = (/) )
24 19 fveq2d 
 |-  ( -. M e. _V -> ( Base ` A ) = ( Base ` (/) ) )
25 2 24 syl5eq 
 |-  ( -. M e. _V -> B = ( Base ` (/) ) )
26 base0 
 |-  (/) = ( Base ` (/) )
27 25 26 eqtr4di 
 |-  ( -. M e. _V -> B = (/) )
28 27 olcd 
 |-  ( -. M e. _V -> ( B = (/) \/ B = (/) ) )
29 0mpo0 
 |-  ( ( B = (/) \/ B = (/) ) -> ( x e. B , y e. B |-> ( x o. y ) ) = (/) )
30 28 29 syl 
 |-  ( -. M e. _V -> ( x e. B , y e. B |-> ( x o. y ) ) = (/) )
31 23 30 eqtr4d 
 |-  ( -. M e. _V -> ( .r ` A ) = ( x e. B , y e. B |-> ( x o. y ) ) )
32 17 31 pm2.61i 
 |-  ( .r ` A ) = ( x e. B , y e. B |-> ( x o. y ) )