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

Metamath Proof Explorer

Theorem dsndxnmulrndx

Description: The slot for the distance function is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024)

		Ref	Expression
	Assertion	dsndxnmulrndx	$⊢ dist (ndx) \neq \cdot_{ndx}$

Proof

Step	Hyp	Ref	Expression
1		3re	$⊢ 3 \in ℝ$
2		1nn	$⊢ 1 \in ℕ$
3		2nn0	$⊢ 2 \in ℕ_{0}$
4		3nn0	$⊢ 3 \in ℕ_{0}$
5		3lt10	$⊢ 3 < 10$
6	2 3 4 5	declti	$⊢ 3 < 12$
7	1 6	gtneii	$⊢ 12 \neq 3$
8		dsndx	$⊢ dist (ndx) = 12$
9		mulrndx	$⊢ \cdot_{ndx} = 3$
10	8 9	neeq12i	$⊢ dist (ndx) \neq \cdot_{ndx} \leftrightarrow 12 \neq 3$
11	7 10	mpbir	$⊢ dist (ndx) \neq \cdot_{ndx}$