Metamath Proof Explorer

Theorem mendbas

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

Ref Expression
Hypothesis mendbas.a 
|- A = ( MEndo ` M )
Assertion mendbas 
|- ( M LMHom M ) = ( Base ` A )

Proof

Step Hyp Ref Expression
1 mendbas.a 
 |-  A = ( MEndo ` M )
2 ovex 
 |-  ( M LMHom M ) e. _V
3 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 ) ) >. } )
4 3 algbase 
 |-  ( ( M LMHom M ) e. _V -> ( M LMHom M ) = ( Base ` ( { <. ( 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 2 4 mp1i 
 |-  ( M e. _V -> ( M LMHom M ) = ( Base ` ( { <. ( 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 eqid 
 |-  ( M LMHom M ) = ( M LMHom M )
7 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 ) )
8 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 ) )
9 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
10 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 ) )
11 6 7 8 9 10 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 ) ) >. } ) )
12 1 11 syl5eq 
 |-  ( M e. _V -> A = ( { <. ( 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 -> ( Base ` A ) = ( Base ` ( { <. ( 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 5 13 eqtr4d 
 |-  ( M e. _V -> ( M LMHom M ) = ( Base ` A ) )
15 base0 
 |-  (/) = ( Base ` (/) )
16 reldmlmhm 
 |-  Rel dom LMHom
17 16 ovprc1 
 |-  ( -. M e. _V -> ( M LMHom M ) = (/) )
18 fvprc 
 |-  ( -. M e. _V -> ( MEndo ` M ) = (/) )
19 1 18 syl5eq 
 |-  ( -. M e. _V -> A = (/) )
20 19 fveq2d 
 |-  ( -. M e. _V -> ( Base ` A ) = ( Base ` (/) ) )
21 15 17 20 3eqtr4a 
 |-  ( -. M e. _V -> ( M LMHom M ) = ( Base ` A ) )
22 14 21 pm2.61i 
 |-  ( M LMHom M ) = ( Base ` A )