Metamath Proof Explorer


Theorem tngsca

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

Ref Expression
Hypotheses tngbas.t 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
tngsca.2 𝐹 = ( Scalar ‘ 𝐺 )
Assertion tngsca ( 𝑁𝑉𝐹 = ( Scalar ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 tngbas.t 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 tngsca.2 𝐹 = ( Scalar ‘ 𝐺 )
3 df-sca Scalar = Slot 5
4 5nn 5 ∈ ℕ
5 5lt9 5 < 9
6 1 3 4 5 tnglem ( 𝑁𝑉 → ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝑇 ) )
7 2 6 syl5eq ( 𝑁𝑉𝐹 = ( Scalar ‘ 𝑇 ) )