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

Metamath Proof Explorer

Theorem ho0coi

Description: Composition of the zero operator and a Hilbert space operator. (Contributed by NM, 9-Aug-2006) (New usage is discouraged.)

Ref Expression
Hypothesis hoaddrid.1 ⊢ T : ℋ ⟶ ℋ
Assertion ho0coi ⊢ 0 hop ∘ T = 0 hop

Proof

Step Hyp Ref Expression
1 hoaddrid.1 ⊢ T : ℋ ⟶ ℋ
2 1 ffvelcdmi ⊢ x ∈ ℋ → T ⁡ x ∈ ℋ
3 ho0val ⊢ T ⁡ x ∈ ℋ → 0 hop ⁡ T ⁡ x = 0 ℎ
4 2 3 syl ⊢ x ∈ ℋ → 0 hop ⁡ T ⁡ x = 0 ℎ
5 ho0f ⊢ 0 hop : ℋ ⟶ ℋ
6 5 1 hocoi ⊢ x ∈ ℋ → 0 hop ∘ T ⁡ x = 0 hop ⁡ T ⁡ x
7 ho0val ⊢ x ∈ ℋ → 0 hop ⁡ x = 0 ℎ
8 4 6 7 3eqtr4d ⊢ x ∈ ℋ → 0 hop ∘ T ⁡ x = 0 hop ⁡ x
9 8 rgen ⊢ ∀ x ∈ ℋ 0 hop ∘ T ⁡ x = 0 hop ⁡ x
10 5 1 hocofi ⊢ 0 hop ∘ T : ℋ ⟶ ℋ
11 10 5 hoeqi ⊢ ∀ x ∈ ℋ 0 hop ∘ T ⁡ x = 0 hop ⁡ x ↔ 0 hop ∘ T = 0 hop
12 9 11 mpbi ⊢ 0 hop ∘ T = 0 hop