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=MEndoM
Assertion mendbas MLMHomM=BaseA

Proof

Step Hyp Ref Expression
1 mendbas.a A=MEndoM
2 ovex MLMHomMV
3 eqid BasendxMLMHomM+ndxxMLMHomM,yMLMHomMx+MfyndxxMLMHomM,yMLMHomMxyScalarndxScalarMndxxBaseScalarM,yMLMHomMBaseM×xMfy=BasendxMLMHomM+ndxxMLMHomM,yMLMHomMx+MfyndxxMLMHomM,yMLMHomMxyScalarndxScalarMndxxBaseScalarM,yMLMHomMBaseM×xMfy
4 3 algbase MLMHomMVMLMHomM=BaseBasendxMLMHomM+ndxxMLMHomM,yMLMHomMx+MfyndxxMLMHomM,yMLMHomMxyScalarndxScalarMndxxBaseScalarM,yMLMHomMBaseM×xMfy
5 2 4 mp1i MVMLMHomM=BaseBasendxMLMHomM+ndxxMLMHomM,yMLMHomMx+MfyndxxMLMHomM,yMLMHomMxyScalarndxScalarMndxxBaseScalarM,yMLMHomMBaseM×xMfy
6 eqid MLMHomM=MLMHomM
7 eqid xMLMHomM,yMLMHomMx+Mfy=xMLMHomM,yMLMHomMx+Mfy
8 eqid xMLMHomM,yMLMHomMxy=xMLMHomM,yMLMHomMxy
9 eqid ScalarM=ScalarM
10 eqid xBaseScalarM,yMLMHomMBaseM×xMfy=xBaseScalarM,yMLMHomMBaseM×xMfy
11 6 7 8 9 10 mendval MVMEndoM=BasendxMLMHomM+ndxxMLMHomM,yMLMHomMx+MfyndxxMLMHomM,yMLMHomMxyScalarndxScalarMndxxBaseScalarM,yMLMHomMBaseM×xMfy
12 1 11 eqtrid MVA=BasendxMLMHomM+ndxxMLMHomM,yMLMHomMx+MfyndxxMLMHomM,yMLMHomMxyScalarndxScalarMndxxBaseScalarM,yMLMHomMBaseM×xMfy
13 12 fveq2d MVBaseA=BaseBasendxMLMHomM+ndxxMLMHomM,yMLMHomMx+MfyndxxMLMHomM,yMLMHomMxyScalarndxScalarMndxxBaseScalarM,yMLMHomMBaseM×xMfy
14 5 13 eqtr4d MVMLMHomM=BaseA
15 base0 =Base
16 reldmlmhm ReldomLMHom
17 16 ovprc1 ¬MVMLMHomM=
18 fvprc ¬MVMEndoM=
19 1 18 eqtrid ¬MVA=
20 19 fveq2d ¬MVBaseA=Base
21 15 17 20 3eqtr4a ¬MVMLMHomM=BaseA
22 14 21 pm2.61i MLMHomM=BaseA