Metamath Proof Explorer


Theorem tngsca

Description: The scalar ring 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 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
tngsca.2 𝐹 = ( Scalar ‘ 𝐺 )
Assertion tngsca ( 𝑁𝑉𝐹 = ( Scalar ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 tngbas.t 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 tngsca.2 𝐹 = ( Scalar ‘ 𝐺 )
3 scaid Scalar = Slot ( Scalar ‘ ndx )
4 slotstnscsi ( ( TopSet ‘ ndx ) ≠ ( Scalar ‘ ndx ) ∧ ( TopSet ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( TopSet ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) )
5 4 simp1i ( TopSet ‘ ndx ) ≠ ( Scalar ‘ ndx )
6 5 necomi ( Scalar ‘ ndx ) ≠ ( TopSet ‘ ndx )
7 slotsdnscsi ( ( dist ‘ ndx ) ≠ ( Scalar ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) )
8 7 simp1i ( dist ‘ ndx ) ≠ ( Scalar ‘ ndx )
9 8 necomi ( Scalar ‘ ndx ) ≠ ( dist ‘ ndx )
10 1 3 6 9 tnglem ( 𝑁𝑉 → ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝑇 ) )
11 2 10 eqtrid ( 𝑁𝑉𝐹 = ( Scalar ‘ 𝑇 ) )