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

Metamath Proof Explorer

Theorem ipndxnbasendx

Description: The slot for the inner product is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024)

Ref Expression
Assertion ipndxnbasendx ⊢ ⋅ 𝑖 ⁡ ndx ≠ Base ndx

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 1lt8 ⊢ 1 < 8
3 1 2 gtneii ⊢ 8 ≠ 1
4 ipndx ⊢ ⋅ 𝑖 ⁡ ndx = 8
5 basendx ⊢ Base ndx = 1
6 4 5 neeq12i ⊢ ⋅ 𝑖 ⁡ ndx ≠ Base ndx ↔ 8 ≠ 1
7 3 6 mpbir ⊢ ⋅ 𝑖 ⁡ ndx ≠ Base ndx