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	⊢ 𝐺 = ( toTG ‘ 𝐻 )
	ttgbas.1	⊢ 𝐵 = ( Base ‘ 𝐻 )
Assertion	ttgbas	⊢ 𝐵 = ( Base ‘ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
2		ttgbas.1	⊢ 𝐵 = ( Base ‘ 𝐻 )
3		baseid	⊢ Base = Slot ( Base ‘ ndx )
4		slotslnbpsd	⊢ ( ( ( LineG ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( LineG ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( LineG ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( LineG ‘ ndx ) ≠ ( dist ‘ ndx ) ) )
5		simpll	⊢ ( ( ( ( LineG ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( LineG ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( LineG ‘ ndx ) ≠ ( ·𝑠 ‘ 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 ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( dist ‘ ndx ) ) )
9		simpll	⊢ ( ( ( ( Itv ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( Itv ‘ ndx ) ≠ ( ·𝑠 ‘ 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 ‘ 𝐻 ) = ( Base ‘ 𝐺 )
13	2 12	eqtri	⊢ 𝐵 = ( Base ‘ 𝐺 )