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 ndxndx

Proof

Step Hyp Ref Expression
1 3re 3
2 3lt6 3<6
3 1 2 gtneii 63
4 vscandx ndx=6
5 mulrndx ndx=3
6 4 5 neeq12i ndxndx63
7 3 6 mpbir ndxndx