Theorem ttgplusg

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

	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		df-plusg	$$⊢{+}_{𝑔}=\mathrm{Slot}2$$
4		2nn	$$⊢2\in \mathbb{N}$$
5		1nn	$$⊢1\in \mathbb{N}$$
6		6nn0	$$⊢6\in {\mathbb{N}}_0$$
7		2nn0	$$⊢2\in {\mathbb{N}}_0$$
8		2lt10	$$⊢2<10$$
9	5 6 7 8	declti	$$⊢2<16$$
10	1 3 4 9	ttglem	$$⊢{+}_H={+}_G$$
11	2 10	eqtri	$$⊢\underset{\dot{}}{+}={+}_G$$