This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ≠ ( +g ‘ ndx )

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 2lt6 ⊢ 2 < 6
3 1 2 gtneii ⊢ 6 ≠ 2
4 vscandx ⊢ ( ·𝑠 ‘ ndx ) = 6
5 plusgndx ⊢ ( +g ‘ ndx ) = 2
6 4 5 neeq12i ⊢ ( ( ·𝑠 ‘ ndx ) ≠ ( +g ‘ ndx ) ↔ 6 ≠ 2 )
7 3 6 mpbir ⊢ ( ·𝑠 ‘ ndx ) ≠ ( +g ‘ ndx )