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