Description: Define the zero vector of Hilbert space. Note that 0vec is considered a primitive in the Hilbert space axioms below, and we don't use this definition outside of this section. It is proved from the axioms as theorem hh0v . (Contributed by NM, 31-May-2008) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | df-h0v | ⊢ 0_{ℎ} = ( 0_{vec} ‘ ⟨ ⟨ +_{ℎ} , ·_{ℎ} ⟩ , norm_{ℎ} ⟩ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | c0v | ⊢ 0_{ℎ} | |
1 | cn0v | ⊢ 0_{vec} | |
2 | cva | ⊢ +_{ℎ} | |
3 | csm | ⊢ ·_{ℎ} | |
4 | 2 3 | cop | ⊢ ⟨ +_{ℎ} , ·_{ℎ} ⟩ |
5 | cno | ⊢ norm_{ℎ} | |
6 | 4 5 | cop | ⊢ ⟨ ⟨ +_{ℎ} , ·_{ℎ} ⟩ , norm_{ℎ} ⟩ |
7 | 6 1 | cfv | ⊢ ( 0_{vec} ‘ ⟨ ⟨ +_{ℎ} , ·_{ℎ} ⟩ , norm_{ℎ} ⟩ ) |
8 | 0 7 | wceq | ⊢ 0_{ℎ} = ( 0_{vec} ‘ ⟨ ⟨ +_{ℎ} , ·_{ℎ} ⟩ , norm_{ℎ} ⟩ ) |