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={to𝒢}_{\mathrm{Tarski}}\left(H\right)$$
	ttgbas.1	$$⊢B={\mathrm{Base}}_H$$
Assertion	ttgbas	$$⊢B={\mathrm{Base}}_G$$

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	$$⊢G={to𝒢}_{\mathrm{Tarski}}\left(H\right)$$
2		ttgbas.1	$$⊢B={\mathrm{Base}}_H$$
3		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
4		slotslnbpsd	$$⊢\left(\left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)$$
5		simpll	$$⊢\left(\left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)\to {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
6	4 5	ax-mp	$$⊢{Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
7	6	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {Line}_{𝒢}\left(\mathrm{ndx}\right)$$
8		slotsinbpsd	$$⊢\left(\left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)$$
9		simpll	$$⊢\left(\left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)\to \mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
10	8 9	ax-mp	$$⊢\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
11	10	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Itv}\left(\mathrm{ndx}\right)$$
12	1 3 7 11	ttglem	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_G$$
13	2 12	eqtri	$$⊢B={\mathrm{Base}}_G$$