Description: Hilbert vector space associative law for subtraction. (Contributed by NM, 7-Oct-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hvass.1 | |- A e. ~H |
|
hvass.2 | |- B e. ~H |
||
hvass.3 | |- C e. ~H |
||
Assertion | hvsubassi | |- ( ( A -h B ) -h C ) = ( A -h ( B +h C ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hvass.1 | |- A e. ~H |
|
2 | hvass.2 | |- B e. ~H |
|
3 | hvass.3 | |- C e. ~H |
|
4 | hvsubass | |- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) -h C ) = ( A -h ( B +h C ) ) ) |
|
5 | 1 2 3 4 | mp3an | |- ( ( A -h B ) -h C ) = ( A -h ( B +h C ) ) |