Metamath Proof Explorer

Theorem mendplusgfval

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

Ref Expression
Hypotheses mendplusgfval.a 
|- A = ( MEndo ` M )
mendplusgfval.b 
|- B = ( Base ` A )
mendplusgfval.p 
|- .+ = ( +g ` M )
Assertion mendplusgfval 
|- ( +g ` A ) = ( x e. B , y e. B |-> ( x oF .+ y ) )

Proof

Step Hyp Ref Expression
1 mendplusgfval.a 
 |-  A = ( MEndo ` M )
2 mendplusgfval.b 
 |-  B = ( Base ` A )
3 mendplusgfval.p 
 |-  .+ = ( +g ` M )
4 1 mendbas 
 |-  ( M LMHom M ) = ( Base ` A )
5 2 4 eqtr4i 
 |-  B = ( M LMHom M )
6 ofeq 
 |-  ( .+ = ( +g ` M ) -> oF .+ = oF ( +g ` M ) )
7 3 6 ax-mp 
 |-  oF .+ = oF ( +g ` M )
8 7 oveqi 
 |-  ( x oF .+ y ) = ( x oF ( +g ` M ) y )
9 8 a1i 
 |-  ( ( x e. B /\ y e. B ) -> ( x oF .+ y ) = ( x oF ( +g ` M ) y ) )
10 9 mpoeq3ia 
 |-  ( x e. B , y e. B |-> ( x oF .+ 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 
 |-  ( Scalar ` M ) = ( Scalar ` M )
13 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 ) )
14 5 10 11 12 13 mendval 
 |-  ( M e. _V -> ( MEndo ` M ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( x e. B , y e. B |-> ( x oF .+ 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 1 14 syl5eq 
 |-  ( M e. _V -> A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( x e. B , y e. B |-> ( x oF .+ 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 15 fveq2d 
 |-  ( M e. _V -> ( +g ` A ) = ( +g ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( x e. B , y e. B |-> ( x oF .+ 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 2 fvexi 
 |-  B e. _V
18 17 17 mpoex 
 |-  ( x e. B , y e. B |-> ( x oF .+ y ) ) e. _V
19 eqid 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( x e. B , y e. B |-> ( x oF .+ 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 .+ 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 ) ) >. } )
20 19 algaddg 
 |-  ( ( x e. B , y e. B |-> ( x oF .+ y ) ) e. _V -> ( x e. B , y e. B |-> ( x oF .+ y ) ) = ( +g ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( x e. B , y e. B |-> ( x oF .+ 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 ) ) >. } ) ) )
21 18 20 mp1i 
 |-  ( M e. _V -> ( x e. B , y e. B |-> ( x oF .+ y ) ) = ( +g ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( x e. B , y e. B |-> ( x oF .+ 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 ) ) >. } ) ) )
22 16 21 eqtr4d 
 |-  ( M e. _V -> ( +g ` A ) = ( x e. B , y e. B |-> ( x oF .+ y ) ) )
23 fvprc 
 |-  ( -. M e. _V -> ( MEndo ` M ) = (/) )
24 1 23 syl5eq 
 |-  ( -. M e. _V -> A = (/) )
25 24 fveq2d 
 |-  ( -. M e. _V -> ( +g ` A ) = ( +g ` (/) ) )
26 df-plusg 
 |-  +g = Slot 2
27 26 str0 
 |-  (/) = ( +g ` (/) )
28 25 27 eqtr4di 
 |-  ( -. M e. _V -> ( +g ` A ) = (/) )
29 24 fveq2d 
 |-  ( -. M e. _V -> ( Base ` A ) = ( Base ` (/) ) )
30 base0 
 |-  (/) = ( Base ` (/) )
31 29 2 30 3eqtr4g 
 |-  ( -. M e. _V -> B = (/) )
32 31 olcd 
 |-  ( -. M e. _V -> ( B = (/) \/ B = (/) ) )
33 0mpo0 
 |-  ( ( B = (/) \/ B = (/) ) -> ( x e. B , y e. B |-> ( x oF .+ y ) ) = (/) )
34 32 33 syl 
 |-  ( -. M e. _V -> ( x e. B , y e. B |-> ( x oF .+ y ) ) = (/) )
35 28 34 eqtr4d 
 |-  ( -. M e. _V -> ( +g ` A ) = ( x e. B , y e. B |-> ( x oF .+ y ) ) )
36 22 35 pm2.61i 
 |-  ( +g ` A ) = ( x e. B , y e. B |-> ( x oF .+ y ) )