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 }_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$

Proof

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