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 ) ≠ ( +g ‘ ndx )

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 1nn ⊢ 1 ∈ ℕ
3 2nn0 ⊢ 2 ∈ ℕ0
4 2lt10 ⊢ 2 < 1 0
5 2 3 3 4 declti ⊢ 2 < 1 2
6 1 5 gtneii ⊢ 1 2 ≠ 2
7 dsndx ⊢ ( dist ‘ ndx ) = 1 2
8 plusgndx ⊢ ( +g ‘ ndx ) = 2
9 7 8 neeq12i ⊢ ( ( dist ‘ ndx ) ≠ ( +g ‘ ndx ) ↔ 1 2 ≠ 2 )
10 6 9 mpbir ⊢ ( dist ‘ ndx ) ≠ ( +g ‘ ndx )