Metamath Proof Explorer


Theorem tngbas

Description: The base set 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 𝑁 )
tngbas.2 𝐵 = ( Base ‘ 𝐺 )
Assertion tngbas ( 𝑁𝑉𝐵 = ( Base ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 tngbas.t 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 tngbas.2 𝐵 = ( Base ‘ 𝐺 )
3 baseid Base = Slot ( Base ‘ ndx )
4 tsetndxnbasendx ( TopSet ‘ ndx ) ≠ ( Base ‘ ndx )
5 4 necomi ( Base ‘ ndx ) ≠ ( TopSet ‘ ndx )
6 dsndxnbasendx ( dist ‘ ndx ) ≠ ( Base ‘ ndx )
7 6 necomi ( Base ‘ ndx ) ≠ ( dist ‘ ndx )
8 1 3 5 7 tnglem ( 𝑁𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑇 ) )
9 2 8 eqtrid ( 𝑁𝑉𝐵 = ( Base ‘ 𝑇 ) )