Metamath Proof Explorer


Theorem vscandxnplusgndx

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

Ref Expression
Assertion vscandxnplusgndx ndx+ndx

Proof

Step Hyp Ref Expression
1 2re 2
2 2lt6 2<6
3 1 2 gtneii 62
4 vscandx ndx=6
5 plusgndx +ndx=2
6 4 5 neeq12i ndx+ndx62
7 3 6 mpbir ndx+ndx