Metamath Proof Explorer


Theorem vscandxnmulrndx

Description: The slot for the scalar product is not the slot for the ring (multiplication) operation in an extensible structure. Formerly part of proof for rmodislmod . (Contributed by AV, 29-Oct-2024)

Ref Expression
Assertion vscandxnmulrndx ( ยท๐‘  โ€˜ ndx ) โ‰  ( .r โ€˜ ndx )

Proof

Step Hyp Ref Expression
1 3re โŠข 3 โˆˆ โ„
2 3lt6 โŠข 3 < 6
3 1 2 gtneii โŠข 6 โ‰  3
4 vscandx โŠข ( ยท๐‘  โ€˜ ndx ) = 6
5 mulrndx โŠข ( .r โ€˜ ndx ) = 3
6 4 5 neeq12i โŠข ( ( ยท๐‘  โ€˜ ndx ) โ‰  ( .r โ€˜ ndx ) โ†” 6 โ‰  3 )
7 3 6 mpbir โŠข ( ยท๐‘  โ€˜ ndx ) โ‰  ( .r โ€˜ ndx )