This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tngvsca

Description: The scalar 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 ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
tngvsca.2 ⊢ · = ( ·𝑠 ‘ 𝐺 )
Assertion tngvsca ( 𝑁 ∈ 𝑉 → · = ( ·𝑠 ‘ 𝑇 ) )

Proof

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