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 e. LinOp
lnopco.2 
|- T e. LinOp
Assertion lnopco0i 
|- ( ( normop ` T ) = 0 -> ( normop ` ( S o. T ) ) = 0 )

Proof

Step Hyp Ref Expression
1 lnopco.1 
 |-  S e. LinOp
2 lnopco.2 
 |-  T e. LinOp
3 coeq2 
 |-  ( T = 0hop -> ( S o. T ) = ( S o. 0hop ) )
4 0lnop 
 |-  0hop e. LinOp
5 1 4 lnopcoi 
 |-  ( S o. 0hop ) e. LinOp
6 5 lnopfi 
 |-  ( S o. 0hop ) : ~H --> ~H
7 ffn 
 |-  ( ( S o. 0hop ) : ~H --> ~H -> ( S o. 0hop ) Fn ~H )
8 6 7 ax-mp 
 |-  ( S o. 0hop ) Fn ~H
9 ho0f 
 |-  0hop : ~H --> ~H
10 ffn 
 |-  ( 0hop : ~H --> ~H -> 0hop Fn ~H )
11 9 10 ax-mp 
 |-  0hop Fn ~H
12 eqfnfv 
 |-  ( ( ( S o. 0hop ) Fn ~H /\ 0hop Fn ~H ) -> ( ( S o. 0hop ) = 0hop <-> A. x e. ~H ( ( S o. 0hop ) ` x ) = ( 0hop ` x ) ) )
13 8 11 12 mp2an 
 |-  ( ( S o. 0hop ) = 0hop <-> A. x e. ~H ( ( S o. 0hop ) ` x ) = ( 0hop ` x ) )
14 ho0val 
 |-  ( x e. ~H -> ( 0hop ` x ) = 0h )
15 14 fveq2d 
 |-  ( x e. ~H -> ( S ` ( 0hop ` x ) ) = ( S ` 0h ) )
16 1 lnop0i 
 |-  ( S ` 0h ) = 0h
17 15 16 eqtrdi 
 |-  ( x e. ~H -> ( S ` ( 0hop ` x ) ) = 0h )
18 1 lnopfi 
 |-  S : ~H --> ~H
19 18 9 hocoi 
 |-  ( x e. ~H -> ( ( S o. 0hop ) ` x ) = ( S ` ( 0hop ` x ) ) )
20 17 19 14 3eqtr4d 
 |-  ( x e. ~H -> ( ( S o. 0hop ) ` x ) = ( 0hop ` x ) )
21 13 20 mprgbir 
 |-  ( S o. 0hop ) = 0hop
22 3 21 eqtrdi 
 |-  ( T = 0hop -> ( S o. T ) = 0hop )
23 2 nmlnop0iHIL 
 |-  ( ( normop ` T ) = 0 <-> T = 0hop )
24 1 2 lnopcoi 
 |-  ( S o. T ) e. LinOp
25 24 nmlnop0iHIL 
 |-  ( ( normop ` ( S o. T ) ) = 0 <-> ( S o. T ) = 0hop )
26 22 23 25 3imtr4i 
 |-  ( ( normop ` T ) = 0 -> ( normop ` ( S o. T ) ) = 0 )