Metamath Proof Explorer

Theorem mendsca

Description: The module endomorphism algebra has the same scalars as the underlying module. (Contributed by Stefan O'Rear, 2-Sep-2015) (Proof shortened by AV, 31-Oct-2024)

Ref Expression
Hypotheses mendsca.a 
|- A = ( MEndo ` M )
mendsca.s 
|- S = ( Scalar ` M )
Assertion mendsca 
|- S = ( Scalar ` A )

Proof

Step Hyp Ref Expression
1 mendsca.a 
 |-  A = ( MEndo ` M )
2 mendsca.s 
 |-  S = ( Scalar ` M )
3 fvex 
 |-  ( Scalar ` M ) e. _V
4 eqid 
 |-  ( { <. ( Base ` ndx ) , ( M LMHom M ) >. , <. ( +g ` ndx ) , ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x oF ( +g ` M ) y ) ) >. , <. ( .r ` ndx ) , ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` M ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` M ) ) , y e. ( M LMHom M ) |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) ) >. } ) = ( { <. ( Base ` ndx ) , ( M LMHom M ) >. , <. ( +g ` ndx ) , ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x oF ( +g ` M ) y ) ) >. , <. ( .r ` ndx ) , ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` M ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` M ) ) , y e. ( M LMHom M ) |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) ) >. } )
5 4 algsca 
 |-  ( ( Scalar ` M ) e. _V -> ( Scalar ` M ) = ( Scalar ` ( { <. ( Base ` ndx ) , ( M LMHom M ) >. , <. ( +g ` ndx ) , ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x oF ( +g ` M ) y ) ) >. , <. ( .r ` ndx ) , ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` M ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` M ) ) , y e. ( M LMHom M ) |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) ) >. } ) ) )
6 3 5 mp1i 
 |-  ( M e. _V -> ( Scalar ` M ) = ( Scalar ` ( { <. ( Base ` ndx ) , ( M LMHom M ) >. , <. ( +g ` ndx ) , ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x oF ( +g ` M ) y ) ) >. , <. ( .r ` ndx ) , ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` M ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` M ) ) , y e. ( M LMHom M ) |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) ) >. } ) ) )
7 eqid 
 |-  ( M LMHom M ) = ( M LMHom M )
8 eqid 
 |-  ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x oF ( +g ` M ) y ) ) = ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x oF ( +g ` M ) y ) )
9 eqid 
 |-  ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x o. y ) ) = ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x o. y ) )
10 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
11 eqid 
 |-  ( x e. ( Base ` ( Scalar ` M ) ) , y e. ( M LMHom M ) |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) ) = ( x e. ( Base ` ( Scalar ` M ) ) , y e. ( M LMHom M ) |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) )
12 7 8 9 10 11 mendval 
 |-  ( M e. _V -> ( MEndo ` M ) = ( { <. ( Base ` ndx ) , ( M LMHom M ) >. , <. ( +g ` ndx ) , ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x oF ( +g ` M ) y ) ) >. , <. ( .r ` ndx ) , ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` M ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` M ) ) , y e. ( M LMHom M ) |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) ) >. } ) )
13 12 fveq2d 
 |-  ( M e. _V -> ( Scalar ` ( MEndo ` M ) ) = ( Scalar ` ( { <. ( Base ` ndx ) , ( M LMHom M ) >. , <. ( +g ` ndx ) , ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x oF ( +g ` M ) y ) ) >. , <. ( .r ` ndx ) , ( x e. ( M LMHom M ) , y e. ( M LMHom M ) |-> ( x o. y ) ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` M ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` ( Scalar ` M ) ) , y e. ( M LMHom M ) |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) ) >. } ) ) )
14 6 13 eqtr4d 
 |-  ( M e. _V -> ( Scalar ` M ) = ( Scalar ` ( MEndo ` M ) ) )
15 scaid 
 |-  Scalar = Slot ( Scalar ` ndx )
16 15 str0 
 |-  (/) = ( Scalar ` (/) )
17 16 eqcomi 
 |-  ( Scalar ` (/) ) = (/)
18 eqid 
 |-  ( MEndo ` M ) = ( MEndo ` M )
19 17 18 fveqprc 
 |-  ( -. M e. _V -> ( Scalar ` M ) = ( Scalar ` ( MEndo ` M ) ) )
20 14 19 pm2.61i 
 |-  ( Scalar ` M ) = ( Scalar ` ( MEndo ` M ) )
21 1 fveq2i 
 |-  ( Scalar ` A ) = ( Scalar ` ( MEndo ` M ) )
22 20 2 21 3eqtr4i 
 |-  S = ( Scalar ` A )