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 ) )