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