Theorem plendxnscandx

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

	Ref	Expression
Assertion	plendxnscandx	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$$

Proof

Step	Hyp	Ref	Expression
1		5re	$$⊢5\in ℝ$$
2		5lt10	$$⊢5<10$$
3	1 2	gtneii	$$⊢10\ne 5$$
4		plendx	$$⊢{\le }_{\mathrm{ndx}}=10$$
5		scandx	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)=5$$
6	4 5	neeq12i	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)\leftrightarrow 10\ne 5$$
7	3 6	mpbir	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$$