Theorem ttgbas

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

	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		baseid	|- Base = Slot ( Base ` ndx )
4		slotslnbpsd	|- ( ( ( LineG ` ndx ) =/= ( Base ` ndx ) /\ ( LineG ` ndx ) =/= ( +g ` ndx ) ) /\ ( ( LineG ` ndx ) =/= ( .s ` ndx ) /\ ( LineG ` ndx ) =/= ( dist ` ndx ) ) )
5		simpll	|- ( ( ( ( LineG ` ndx ) =/= ( Base ` ndx ) /\ ( LineG ` ndx ) =/= ( +g ` ndx ) ) /\ ( ( LineG ` ndx ) =/= ( .s ` ndx ) /\ ( LineG ` ndx ) =/= ( dist ` ndx ) ) ) -> ( LineG ` ndx ) =/= ( Base ` ndx ) )
6	4 5	ax-mp	|- ( LineG ` ndx ) =/= ( Base ` ndx )
7	6	necomi	|- ( Base ` ndx ) =/= ( LineG ` ndx )
8		slotsinbpsd	|- ( ( ( Itv ` ndx ) =/= ( Base ` ndx ) /\ ( Itv ` ndx ) =/= ( +g ` ndx ) ) /\ ( ( Itv ` ndx ) =/= ( .s ` ndx ) /\ ( Itv ` ndx ) =/= ( dist ` ndx ) ) )
9		simpll	|- ( ( ( ( Itv ` ndx ) =/= ( Base ` ndx ) /\ ( Itv ` ndx ) =/= ( +g ` ndx ) ) /\ ( ( Itv ` ndx ) =/= ( .s ` ndx ) /\ ( Itv ` ndx ) =/= ( dist ` ndx ) ) ) -> ( Itv ` ndx ) =/= ( Base ` ndx ) )
10	8 9	ax-mp	|- ( Itv ` ndx ) =/= ( Base ` ndx )
11	10	necomi	|- ( Base ` ndx ) =/= ( Itv ` ndx )
12	1 3 7 11	ttglem	|- ( Base ` H ) = ( Base ` G )
13	2 12	eqtri	|- B = ( Base ` G )