Theorem ttgvsca

Description: The scalar product 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)$$
	ttgvsca.1	$$⊢\underset{\dot{}}{·}={\cdot }_H$$
Assertion	ttgvsca	$$⊢\underset{\dot{}}{·}={\cdot }_G$$

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	$$⊢G={to𝒢}_{\mathrm{Tarski}}\left(H\right)$$
2		ttgvsca.1	$$⊢\underset{\dot{}}{·}={\cdot }_H$$
3		df-vsca	$$⊢{\cdot }_{𝑠}=\mathrm{Slot}6$$
4		6nn	$$⊢6\in \mathbb{N}$$
5		1nn	$$⊢1\in \mathbb{N}$$
6		6nn0	$$⊢6\in {\mathbb{N}}_0$$
7		6lt10	$$⊢6<10$$
8	5 6 6 7	declti	$$⊢6<16$$
9	1 3 4 8	ttglem	$$⊢{\cdot }_H={\cdot }_G$$
10	2 9	eqtri	$$⊢\underset{\dot{}}{·}={\cdot }_G$$