Metamath Proof Explorer


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 = ( toTG ` H )
ttgsub.1
|- .- = ( -g ` H )
Assertion ttgsub
|- .- = ( -g ` G )

Proof

Step Hyp Ref Expression
1 ttgval.n
 |-  G = ( toTG ` H )
2 ttgsub.1
 |-  .- = ( -g ` H )
3 eqid
 |-  ( Base ` H ) = ( Base ` H )
4 1 3 ttgbas
 |-  ( Base ` H ) = ( Base ` G )
5 4 a1i
 |-  ( T. -> ( Base ` H ) = ( Base ` G ) )
6 eqid
 |-  ( +g ` H ) = ( +g ` H )
7 1 6 ttgplusg
 |-  ( +g ` H ) = ( +g ` G )
8 7 a1i
 |-  ( T. -> ( +g ` H ) = ( +g ` G ) )
9 5 8 grpsubpropd
 |-  ( T. -> ( -g ` H ) = ( -g ` G ) )
10 9 mptru
 |-  ( -g ` H ) = ( -g ` G )
11 2 10 eqtri
 |-  .- = ( -g ` G )