Description: Obsolete version of mnringaddgd as of 1-Nov-2024. The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mnringaddgd.1 | |- F = ( R MndRing M ) |
|
| mnringaddgd.2 | |- A = ( Base ` M ) |
||
| mnringaddgd.3 | |- V = ( R freeLMod A ) |
||
| mnringaddgd.4 | |- ( ph -> R e. U ) |
||
| mnringaddgd.5 | |- ( ph -> M e. W ) |
||
| Assertion | mnringaddgdOLD | |- ( ph -> ( +g ` V ) = ( +g ` F ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mnringaddgd.1 | |- F = ( R MndRing M ) |
|
| 2 | mnringaddgd.2 | |- A = ( Base ` M ) |
|
| 3 | mnringaddgd.3 | |- V = ( R freeLMod A ) |
|
| 4 | mnringaddgd.4 | |- ( ph -> R e. U ) |
|
| 5 | mnringaddgd.5 | |- ( ph -> M e. W ) |
|
| 6 | df-plusg | |- +g = Slot 2 |
|
| 7 | 2nn | |- 2 e. NN |
|
| 8 | 2re | |- 2 e. RR |
|
| 9 | 2lt3 | |- 2 < 3 |
|
| 10 | 8 9 | ltneii | |- 2 =/= 3 |
| 11 | mulrndx | |- ( .r ` ndx ) = 3 |
|
| 12 | 10 11 | neeqtrri | |- 2 =/= ( .r ` ndx ) |
| 13 | 1 6 7 12 2 3 4 5 | mnringnmulrdOLD | |- ( ph -> ( +g ` V ) = ( +g ` F ) ) |