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

Metamath Proof Explorer

Theorem slotsdifipndx

Description: The slot for the scalar is not the index of other slots. Formerly part of proof for srasca and sravsca . (Contributed by AV, 12-Nov-2024)

Ref Expression
Assertion slotsdifipndx ( ( ·𝑠 ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) ∧ ( Scalar ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) )

Proof

Step Hyp Ref Expression
1 6re ⊢ 6 ∈ ℝ
2 6lt8 ⊢ 6 < 8
3 1 2 ltneii ⊢ 6 ≠ 8
4 vscandx ⊢ ( ·𝑠 ‘ ndx ) = 6
5 ipndx ⊢ ( ·𝑖 ‘ ndx ) = 8
6 4 5 neeq12i ⊢ ( ( ·𝑠 ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) ↔ 6 ≠ 8 )
7 3 6 mpbir ⊢ ( ·𝑠 ‘ ndx ) ≠ ( ·𝑖 ‘ ndx )
8 5re ⊢ 5 ∈ ℝ
9 5lt8 ⊢ 5 < 8
10 8 9 ltneii ⊢ 5 ≠ 8
11 scandx ⊢ ( Scalar ‘ ndx ) = 5
12 11 5 neeq12i ⊢ ( ( Scalar ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) ↔ 5 ≠ 8 )
13 10 12 mpbir ⊢ ( Scalar ‘ ndx ) ≠ ( ·𝑖 ‘ ndx )
14 7 13 pm3.2i ⊢ ( ( ·𝑠 ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) ∧ ( Scalar ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) )