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 ⊢ 𝑇 : ℋ ⟶ ℋ
Assertion ho0coi ( 0hop ∘ 𝑇 ) = 0hop

Proof

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