Metamath Proof Explorer


Theorem ttgbas

Description: The base set of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019)

Ref Expression
Hypotheses ttgval.n
|- G = ( toTG ` H )
ttgbas.1
|- B = ( Base ` H )
Assertion ttgbas
|- B = ( Base ` G )

Proof

Step Hyp Ref Expression
1 ttgval.n
 |-  G = ( toTG ` H )
2 ttgbas.1
 |-  B = ( Base ` H )
3 df-base
 |-  Base = Slot 1
4 1nn
 |-  1 e. NN
5 6nn0
 |-  6 e. NN0
6 1nn0
 |-  1 e. NN0
7 1lt10
 |-  1 < ; 1 0
8 4 5 6 7 declti
 |-  1 < ; 1 6
9 1 3 4 8 ttglem
 |-  ( Base ` H ) = ( Base ` G )
10 2 9 eqtri
 |-  B = ( Base ` G )