Description: Hilbert vector space commutative/associative law. (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 | hvsub32i | |- ( ( A -h B ) -h C ) = ( ( A -h C ) -h B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hvass.1 | |- A e. ~H |
|
2 | hvass.2 | |- B e. ~H |
|
3 | hvass.3 | |- C e. ~H |
|
4 | hvsub32 | |- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) -h C ) = ( ( A -h C ) -h B ) ) |
|
5 | 1 2 3 4 | mp3an | |- ( ( A -h B ) -h C ) = ( ( A -h C ) -h B ) |