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	⊢ 𝐺 = ( toTG ‘ 𝐻 )
	ttgplusg.1	⊢ + = ( +g ‘ 𝐻 )
Assertion	ttgplusg	⊢ + = ( +g ‘ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
2		ttgplusg.1	⊢ + = ( +g ‘ 𝐻 )
3		df-plusg	⊢ +g = Slot 2
4		2nn	⊢ 2 ∈ ℕ
5		1nn	⊢ 1 ∈ ℕ
6		6nn0	⊢ 6 ∈ ℕ0
7		2nn0	⊢ 2 ∈ ℕ0
8		2lt10	⊢ 2 < ; 1 0
9	5 6 7 8	declti	⊢ 2 < ; 1 6
10	1 3 4 9	ttglem	⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐺 )
11	2 10	eqtri	⊢ + = ( +g ‘ 𝐺 )