Metamath Proof Explorer


Theorem tngmulr

Description: The ring multiplication 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 )
tngmulr.2
|- .x. = ( .r ` G )
Assertion tngmulr
|- ( N e. V -> .x. = ( .r ` T ) )

Proof

Step Hyp Ref Expression
1 tngbas.t
 |-  T = ( G toNrmGrp N )
2 tngmulr.2
 |-  .x. = ( .r ` G )
3 mulrid
 |-  .r = Slot ( .r ` ndx )
4 tsetndxnmulrndx
 |-  ( TopSet ` ndx ) =/= ( .r ` ndx )
5 4 necomi
 |-  ( .r ` ndx ) =/= ( TopSet ` ndx )
6 dsndxnmulrndx
 |-  ( dist ` ndx ) =/= ( .r ` ndx )
7 6 necomi
 |-  ( .r ` ndx ) =/= ( dist ` ndx )
8 1 3 5 7 tnglem
 |-  ( N e. V -> ( .r ` G ) = ( .r ` T ) )
9 2 8 eqtrid
 |-  ( N e. V -> .x. = ( .r ` T ) )