# 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 hoaddid1.1 ${⊢}{T}:ℋ⟶ℋ$
Assertion ho0coi ${⊢}{0}_{\mathrm{hop}}\circ {T}={0}_{\mathrm{hop}}$

### Proof

Step Hyp Ref Expression
1 hoaddid1.1 ${⊢}{T}:ℋ⟶ℋ$
2 1 ffvelrni ${⊢}{x}\in ℋ\to {T}\left({x}\right)\in ℋ$
3 ho0val ${⊢}{T}\left({x}\right)\in ℋ\to {0}_{\mathrm{hop}}\left({T}\left({x}\right)\right)={0}_{ℎ}$
4 2 3 syl ${⊢}{x}\in ℋ\to {0}_{\mathrm{hop}}\left({T}\left({x}\right)\right)={0}_{ℎ}$
5 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
6 5 1 hocoi ${⊢}{x}\in ℋ\to \left({0}_{\mathrm{hop}}\circ {T}\right)\left({x}\right)={0}_{\mathrm{hop}}\left({T}\left({x}\right)\right)$
7 ho0val ${⊢}{x}\in ℋ\to {0}_{\mathrm{hop}}\left({x}\right)={0}_{ℎ}$
8 4 6 7 3eqtr4d ${⊢}{x}\in ℋ\to \left({0}_{\mathrm{hop}}\circ {T}\right)\left({x}\right)={0}_{\mathrm{hop}}\left({x}\right)$
9 8 rgen ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({0}_{\mathrm{hop}}\circ {T}\right)\left({x}\right)={0}_{\mathrm{hop}}\left({x}\right)$
10 5 1 hocofi ${⊢}\left({0}_{\mathrm{hop}}\circ {T}\right):ℋ⟶ℋ$
11 10 5 hoeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({0}_{\mathrm{hop}}\circ {T}\right)\left({x}\right)={0}_{\mathrm{hop}}\left({x}\right)↔{0}_{\mathrm{hop}}\circ {T}={0}_{\mathrm{hop}}$
12 9 11 mpbi ${⊢}{0}_{\mathrm{hop}}\circ {T}={0}_{\mathrm{hop}}$