Metamath Proof Explorer


Theorem scandxnmulrndx

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

Ref Expression
Assertion scandxnmulrndx Scalarndxndx

Proof

Step Hyp Ref Expression
1 3re 3
2 3lt5 3<5
3 1 2 gtneii 53
4 scandx Scalarndx=5
5 mulrndx ndx=3
6 4 5 neeq12i Scalarndxndx53
7 3 6 mpbir Scalarndxndx