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

Metamath Proof Explorer

Theorem tngip

Description: The inner product operation of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 31-Oct-2024)

Ref Expression
Hypotheses tngbas.t 
|- T = ( G toNrmGrp N )
tngip.2 
|- ., = ( .i ` G )
Assertion tngip 
|- ( N e. V -> ., = ( .i ` T ) )

Proof

Step Hyp Ref Expression
1 tngbas.t 
 |-  T = ( G toNrmGrp N )
2 tngip.2 
 |-  ., = ( .i ` G )
3 ipid 
 |-  .i = Slot ( .i ` ndx )
4 slotstnscsi 
 |-  ( ( TopSet ` ndx ) =/= ( Scalar ` ndx ) /\ ( TopSet ` ndx ) =/= ( .s ` ndx ) /\ ( TopSet ` ndx ) =/= ( .i ` ndx ) )
5 4 simp3i 
 |-  ( TopSet ` ndx ) =/= ( .i ` ndx )
6 5 necomi 
 |-  ( .i ` ndx ) =/= ( TopSet ` ndx )
7 slotsdnscsi 
 |-  ( ( dist ` ndx ) =/= ( Scalar ` ndx ) /\ ( dist ` ndx ) =/= ( .s ` ndx ) /\ ( dist ` ndx ) =/= ( .i ` ndx ) )
8 7 simp3i 
 |-  ( dist ` ndx ) =/= ( .i ` ndx )
9 8 necomi 
 |-  ( .i ` ndx ) =/= ( dist ` ndx )
10 1 3 6 9 tnglem 
 |-  ( N e. V -> ( .i ` G ) = ( .i ` T ) )
11 2 10 eqtrid 
 |-  ( N e. V -> ., = ( .i ` T ) )