This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hh0oi

Description: The zero operator in Hilbert space. (Contributed by NM, 7-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses hhnmo.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
hh0o.2 ⊢ Z = U 0 op U
Assertion hh0oi ⊢ 0 hop = Z

Proof

Step Hyp Ref Expression
1 hhnmo.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
2 hh0o.2 ⊢ Z = U 0 op U
3 1 hhba ⊢ ℋ = BaseSet ⁡ U
4 df-ch0 ⊢ 0 ℋ = 0 ℎ
5 1 hh0v ⊢ 0 ℎ = 0 vec ⁡ U
6 5 sneqi ⊢ 0 ℎ = 0 vec ⁡ U
7 4 6 eqtri ⊢ 0 ℋ = 0 vec ⁡ U
8 3 7 xpeq12i ⊢ ℋ × 0 ℋ = BaseSet ⁡ U × 0 vec ⁡ U
9 df0op2 ⊢ 0 hop = ℋ × 0 ℋ
10 1 hhnv ⊢ U ∈ NrmCVec
11 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
12 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
13 11 12 2 0ofval ⊢ U ∈ NrmCVec ∧ U ∈ NrmCVec → Z = BaseSet ⁡ U × 0 vec ⁡ U
14 10 10 13 mp2an ⊢ Z = BaseSet ⁡ U × 0 vec ⁡ U
15 8 9 14 3eqtr4i ⊢ 0 hop = Z