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

Metamath Proof Explorer

Theorem vscandxnmulrndx

Description: The slot for the scalar product is not the slot for the ring (multiplication) operation in an extensible structure. Formerly part of proof for rmodislmod . (Contributed by AV, 29-Oct-2024)

		Ref	Expression
	Assertion	vscandxnmulrndx	$⊢ \cdot_{ndx} \neq \cdot_{ndx}$

Proof

Step	Hyp	Ref	Expression
1		3re	$⊢ 3 \in ℝ$
2		3lt6	$⊢ 3 < 6$
3	1 2	gtneii	$⊢ 6 \neq 3$
4		vscandx	$⊢ \cdot_{ndx} = 6$
5		mulrndx	$⊢ \cdot_{ndx} = 3$
6	4 5	neeq12i	$⊢ \cdot_{ndx} \neq \cdot_{ndx} \leftrightarrow 6 \neq 3$
7	3 6	mpbir	$⊢ \cdot_{ndx} \neq \cdot_{ndx}$