Metamath Proof Explorer
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 ) |