Description: Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | mendbas.a | |
|
Assertion | mendbas | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mendbas.a | |
|
2 | ovex | |
|
3 | eqid | |
|
4 | 3 | algbase | |
5 | 2 4 | mp1i | |
6 | eqid | |
|
7 | eqid | |
|
8 | eqid | |
|
9 | eqid | |
|
10 | eqid | |
|
11 | 6 7 8 9 10 | mendval | |
12 | 1 11 | eqtrid | |
13 | 12 | fveq2d | |
14 | 5 13 | eqtr4d | |
15 | base0 | |
|
16 | reldmlmhm | |
|
17 | 16 | ovprc1 | |
18 | fvprc | |
|
19 | 1 18 | eqtrid | |
20 | 19 | fveq2d | |
21 | 15 17 20 | 3eqtr4a | |
22 | 14 21 | pm2.61i | |