Metamath Proof Explorer


Theorem tngvsca

Description: The scalar multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses tngbas.t T = G toNrmGrp N
tngvsca.2 · ˙ = G
Assertion tngvsca N V · ˙ = T

Proof

Step Hyp Ref Expression
1 tngbas.t T = G toNrmGrp N
2 tngvsca.2 · ˙ = G
3 df-vsca 𝑠 = Slot 6
4 6nn 6
5 6lt9 6 < 9
6 1 3 4 5 tnglem N V G = T
7 2 6 syl5eq N V · ˙ = T