This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = toCPreHil ⁡ W
tcphsub.v ⊢ - ˙ = - W
Assertion tcphsub ⊢ - ˙ = - G

Proof

Step Hyp Ref Expression
1 tcphval.n ⊢ G = toCPreHil ⁡ W
2 tcphsub.v ⊢ - ˙ = - W
3 eqid ⊢ Base W = Base W
4 1 3 tcphbas ⊢ Base W = Base G
5 4 a1i ⊢ ⊤ → Base W = Base G
6 eqid ⊢ + W = + W
7 1 6 tchplusg ⊢ + W = + G
8 7 a1i ⊢ ⊤ → + W = + G
9 5 8 grpsubpropd ⊢ ⊤ → - W = - G
10 9 mptru ⊢ - W = - G
11 2 10 eqtri ⊢ - ˙ = - G