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

Metamath Proof Explorer

Theorem dsndxnplusgndx

Description: The slot for the distance function is not the slot for the group operation in an extensible structure. Formerly part of proof for mgpds . (Contributed by AV, 18-Oct-2024)

		Ref	Expression
	Assertion	dsndxnplusgndx	$⊢ dist (ndx) \neq +_{ndx}$

Proof

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