Theorem ttgplusg

Description: The addition operation 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)$$
	ttgplusg.1	$$⊢\underset{\dot{}}{+}={+}_H$$
Assertion	ttgplusg	$$⊢\underset{\dot{}}{+}={+}_G$$

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	$$⊢G={to𝒢}_{\mathrm{Tarski}}\left(H\right)$$
2		ttgplusg.1	$$⊢\underset{\dot{}}{+}={+}_H$$
3		plusgid	$$⊢{+}_{𝑔}=\mathrm{Slot}{+}_{\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		simplr	$$⊢\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{ndx}}$$
6	4 5	ax-mp	$$⊢{Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}$$
7	6	necomi	$$⊢{+}_{\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		simplr	$$⊢\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{ndx}}$$
10	8 9	ax-mp	$$⊢\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}$$
11	10	necomi	$$⊢{+}_{\mathrm{ndx}}\ne \mathrm{Itv}\left(\mathrm{ndx}\right)$$
12	1 3 7 11	ttglem	$$⊢{+}_H={+}_G$$
13	2 12	eqtri	$$⊢\underset{\dot{}}{+}={+}_G$$