Database
COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)
Axiomatization of complex pre-Hilbert spaces
Vector operations
hvsubassi
Metamath Proof Explorer
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 ∈ ℋ
hvass.2
⊢ B ∈ ℋ
hvass.3
⊢ C ∈ ℋ
Assertion
hvsubassi
⊢ A - ℎ B - ℎ C = A - ℎ B + ℎ C
Proof
Step
Hyp
Ref
Expression
1
hvass.1
⊢ A ∈ ℋ
2
hvass.2
⊢ B ∈ ℋ
3
hvass.3
⊢ C ∈ ℋ
4
hvsubass
⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A - ℎ B - ℎ C = A - ℎ B + ℎ C
5
1 2 3 4
mp3an
⊢ A - ℎ B - ℎ C = A - ℎ B + ℎ C