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 ) |
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 ) |