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 LinOp
lnopco.2 T LinOp
Assertion lnopco0i norm op T = 0 norm op S T = 0

Proof

Step Hyp Ref Expression
1 lnopco.1 S LinOp
2 lnopco.2 T LinOp
3 coeq2 T = 0 hop S T = S 0 hop
4 0lnop 0 hop LinOp
5 1 4 lnopcoi S 0 hop LinOp
6 5 lnopfi S 0 hop :
7 ffn S 0 hop : S 0 hop Fn
8 6 7 ax-mp S 0 hop Fn
9 ho0f 0 hop :
10 ffn 0 hop : 0 hop Fn
11 9 10 ax-mp 0 hop Fn
12 eqfnfv S 0 hop Fn 0 hop Fn S 0 hop = 0 hop x S 0 hop x = 0 hop x
13 8 11 12 mp2an S 0 hop = 0 hop x S 0 hop x = 0 hop x
14 ho0val x 0 hop x = 0
15 14 fveq2d x S 0 hop x = S 0
16 1 lnop0i S 0 = 0
17 15 16 syl6eq x S 0 hop x = 0
18 1 lnopfi S :
19 18 9 hocoi x S 0 hop x = S 0 hop x
20 17 19 14 3eqtr4d x S 0 hop x = 0 hop x
21 13 20 mprgbir S 0 hop = 0 hop
22 3 21 syl6eq T = 0 hop S T = 0 hop
23 2 nmlnop0iHIL norm op T = 0 T = 0 hop
24 1 2 lnopcoi S T LinOp
25 24 nmlnop0iHIL norm op S T = 0 S T = 0 hop
26 22 23 25 3imtr4i norm op T = 0 norm op S T = 0