# Metamath Proof Explorer

## Theorem lnopco0i

Description: The composition of a linear operator with one whose norm is zero. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypotheses lnopco.1 ${⊢}{S}\in \mathrm{LinOp}$
lnopco.2 ${⊢}{T}\in \mathrm{LinOp}$
Assertion lnopco0i ${⊢}{norm}_{\mathrm{op}}\left({T}\right)=0\to {norm}_{\mathrm{op}}\left({S}\circ {T}\right)=0$

### Proof

Step Hyp Ref Expression
1 lnopco.1 ${⊢}{S}\in \mathrm{LinOp}$
2 lnopco.2 ${⊢}{T}\in \mathrm{LinOp}$
3 coeq2 ${⊢}{T}={0}_{\mathrm{hop}}\to {S}\circ {T}={S}\circ {0}_{\mathrm{hop}}$
4 0lnop ${⊢}{0}_{\mathrm{hop}}\in \mathrm{LinOp}$
5 1 4 lnopcoi ${⊢}{S}\circ {0}_{\mathrm{hop}}\in \mathrm{LinOp}$
6 5 lnopfi ${⊢}\left({S}\circ {0}_{\mathrm{hop}}\right):ℋ⟶ℋ$
7 ffn ${⊢}\left({S}\circ {0}_{\mathrm{hop}}\right):ℋ⟶ℋ\to \left({S}\circ {0}_{\mathrm{hop}}\right)Fnℋ$
8 6 7 ax-mp ${⊢}\left({S}\circ {0}_{\mathrm{hop}}\right)Fnℋ$
9 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
10 ffn ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ\to {0}_{\mathrm{hop}}Fnℋ$
11 9 10 ax-mp ${⊢}{0}_{\mathrm{hop}}Fnℋ$
12 eqfnfv ${⊢}\left(\left({S}\circ {0}_{\mathrm{hop}}\right)Fnℋ\wedge {0}_{\mathrm{hop}}Fnℋ\right)\to \left({S}\circ {0}_{\mathrm{hop}}={0}_{\mathrm{hop}}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({S}\circ {0}_{\mathrm{hop}}\right)\left({x}\right)={0}_{\mathrm{hop}}\left({x}\right)\right)$
13 8 11 12 mp2an ${⊢}{S}\circ {0}_{\mathrm{hop}}={0}_{\mathrm{hop}}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({S}\circ {0}_{\mathrm{hop}}\right)\left({x}\right)={0}_{\mathrm{hop}}\left({x}\right)$
14 ho0val ${⊢}{x}\in ℋ\to {0}_{\mathrm{hop}}\left({x}\right)={0}_{ℎ}$
15 14 fveq2d ${⊢}{x}\in ℋ\to {S}\left({0}_{\mathrm{hop}}\left({x}\right)\right)={S}\left({0}_{ℎ}\right)$
16 1 lnop0i ${⊢}{S}\left({0}_{ℎ}\right)={0}_{ℎ}$
17 15 16 syl6eq ${⊢}{x}\in ℋ\to {S}\left({0}_{\mathrm{hop}}\left({x}\right)\right)={0}_{ℎ}$
18 1 lnopfi ${⊢}{S}:ℋ⟶ℋ$
19 18 9 hocoi ${⊢}{x}\in ℋ\to \left({S}\circ {0}_{\mathrm{hop}}\right)\left({x}\right)={S}\left({0}_{\mathrm{hop}}\left({x}\right)\right)$
20 17 19 14 3eqtr4d ${⊢}{x}\in ℋ\to \left({S}\circ {0}_{\mathrm{hop}}\right)\left({x}\right)={0}_{\mathrm{hop}}\left({x}\right)$
21 13 20 mprgbir ${⊢}{S}\circ {0}_{\mathrm{hop}}={0}_{\mathrm{hop}}$
22 3 21 syl6eq ${⊢}{T}={0}_{\mathrm{hop}}\to {S}\circ {T}={0}_{\mathrm{hop}}$
23 2 nmlnop0iHIL ${⊢}{norm}_{\mathrm{op}}\left({T}\right)=0↔{T}={0}_{\mathrm{hop}}$
24 1 2 lnopcoi ${⊢}{S}\circ {T}\in \mathrm{LinOp}$
25 24 nmlnop0iHIL ${⊢}{norm}_{\mathrm{op}}\left({S}\circ {T}\right)=0↔{S}\circ {T}={0}_{\mathrm{hop}}$
26 22 23 25 3imtr4i ${⊢}{norm}_{\mathrm{op}}\left({T}\right)=0\to {norm}_{\mathrm{op}}\left({S}\circ {T}\right)=0$