Metamath Proof Explorer


Theorem ipndxnplusgndx

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

Ref Expression
Assertion ipndxnplusgndx ( ยท๐‘– โ€˜ ndx ) โ‰  ( +g โ€˜ ndx )

Proof

Step Hyp Ref Expression
1 2re โŠข 2 โˆˆ โ„
2 2lt8 โŠข 2 < 8
3 1 2 gtneii โŠข 8 โ‰  2
4 ipndx โŠข ( ยท๐‘– โ€˜ ndx ) = 8
5 plusgndx โŠข ( +g โ€˜ ndx ) = 2
6 4 5 neeq12i โŠข ( ( ยท๐‘– โ€˜ ndx ) โ‰  ( +g โ€˜ ndx ) โ†” 8 โ‰  2 )
7 3 6 mpbir โŠข ( ยท๐‘– โ€˜ ndx ) โ‰  ( +g โ€˜ ndx )