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

Metamath Proof Explorer

Theorem plendxnvscandx

Description: The slot for the "less than or equal to" ordering is not the slot for the scalar product in an extensible structure. Formerly part of proof for opsrvsca . (Contributed by AV, 1-Nov-2024)

Ref Expression
Assertion plendxnvscandx ( le ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )

Proof

Step Hyp Ref Expression
1 6re ⊢ 6 ∈ ℝ
2 6lt10 ⊢ 6 < 1 0
3 1 2 gtneii ⊢ 1 0 ≠ 6
4 plendx ⊢ ( le ‘ ndx ) = 1 0
5 vscandx ⊢ ( ·𝑠 ‘ ndx ) = 6
6 4 5 neeq12i ⊢ ( ( le ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ↔ 1 0 ≠ 6 )
7 3 6 mpbir ⊢ ( le ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )