Theorem tcphsub

Description: The subtraction operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019)

	Ref	Expression
Hypotheses	tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
	tcphsub.v	$$⊢\underset{\dot{}}{-}={-}_W$$
Assertion	tcphsub	$$⊢\underset{\dot{}}{-}={-}_G$$

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
2		tcphsub.v	$$⊢\underset{\dot{}}{-}={-}_W$$
3		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
4	1 3	tcphbas	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_G$$
5	4	a1i	$$⊢\top \to {\mathrm{Base}}_W={\mathrm{Base}}_G$$
6		eqid	$$⊢{+}_W={+}_W$$
7	1 6	tchplusg	$$⊢{+}_W={+}_G$$
8	7	a1i	$$⊢\top \to {+}_W={+}_G$$
9	5 8	grpsubpropd	$$⊢\top \to {-}_W={-}_G$$
10	9	mptru	$$⊢{-}_W={-}_G$$
11	2 10	eqtri	$$⊢\underset{\dot{}}{-}={-}_G$$