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