Theorem ttgsub

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

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	$$⊢G={to𝒢}_{\mathrm{Tarski}}\left(H\right)$$
2		ttgsub.1	$$⊢\underset{\dot{}}{-}={-}_H$$
3		eqid	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_H$$
4	1 3	ttgbas	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_G$$
5	4	a1i	$$⊢\top \to {\mathrm{Base}}_H={\mathrm{Base}}_G$$
6		eqid	$$⊢{+}_H={+}_H$$
7	1 6	ttgplusg	$$⊢{+}_H={+}_G$$
8	7	a1i	$$⊢\top \to {+}_H={+}_G$$
9	5 8	grpsubpropd	$$⊢\top \to {-}_H={-}_G$$
10	9	mptru	$$⊢{-}_H={-}_G$$
11	2 10	eqtri	$$⊢\underset{\dot{}}{-}={-}_G$$