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

Proof

Step	Hyp	Ref	Expression
1		hoaddid1.1	⊢ 𝑇 : ℋ ⟶ ℋ
2	1	ffvelrni	⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
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