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