Metamath Proof Explorer

Theorem lnop0

Description: The value of a linear Hilbert space operator at zero is zero. Remark in Beran p. 99. (Contributed by NM, 13-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion lnop0 
|- ( T e. LinOp -> ( T ` 0h ) = 0h )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 ax-hv0cl 
 |-  0h e. ~H
3 1 2 hvmulcli 
 |-  ( 1 .h 0h ) e. ~H
4 ax-hvaddid 
 |-  ( ( 1 .h 0h ) e. ~H -> ( ( 1 .h 0h ) +h 0h ) = ( 1 .h 0h ) )
5 3 4 ax-mp 
 |-  ( ( 1 .h 0h ) +h 0h ) = ( 1 .h 0h )
6 ax-hvmulid 
 |-  ( 0h e. ~H -> ( 1 .h 0h ) = 0h )
7 2 6 ax-mp 
 |-  ( 1 .h 0h ) = 0h
8 5 7 eqtri 
 |-  ( ( 1 .h 0h ) +h 0h ) = 0h
9 8 fveq2i 
 |-  ( T ` ( ( 1 .h 0h ) +h 0h ) ) = ( T ` 0h )
10 lnopl 
 |-  ( ( ( T e. LinOp /\ 1 e. CC ) /\ ( 0h e. ~H /\ 0h e. ~H ) ) -> ( T ` ( ( 1 .h 0h ) +h 0h ) ) = ( ( 1 .h ( T ` 0h ) ) +h ( T ` 0h ) ) )
11 2 2 10 mpanr12 
 |-  ( ( T e. LinOp /\ 1 e. CC ) -> ( T ` ( ( 1 .h 0h ) +h 0h ) ) = ( ( 1 .h ( T ` 0h ) ) +h ( T ` 0h ) ) )
12 1 11 mpan2 
 |-  ( T e. LinOp -> ( T ` ( ( 1 .h 0h ) +h 0h ) ) = ( ( 1 .h ( T ` 0h ) ) +h ( T ` 0h ) ) )
13 9 12 eqtr3id 
 |-  ( T e. LinOp -> ( T ` 0h ) = ( ( 1 .h ( T ` 0h ) ) +h ( T ` 0h ) ) )
14 lnopf 
 |-  ( T e. LinOp -> T : ~H --> ~H )
15 ffvelrn 
 |-  ( ( T : ~H --> ~H /\ 0h e. ~H ) -> ( T ` 0h ) e. ~H )
16 2 15 mpan2 
 |-  ( T : ~H --> ~H -> ( T ` 0h ) e. ~H )
17 14 16 syl 
 |-  ( T e. LinOp -> ( T ` 0h ) e. ~H )
18 ax-hvmulid 
 |-  ( ( T ` 0h ) e. ~H -> ( 1 .h ( T ` 0h ) ) = ( T ` 0h ) )
19 17 18 syl 
 |-  ( T e. LinOp -> ( 1 .h ( T ` 0h ) ) = ( T ` 0h ) )
20 19 oveq1d 
 |-  ( T e. LinOp -> ( ( 1 .h ( T ` 0h ) ) +h ( T ` 0h ) ) = ( ( T ` 0h ) +h ( T ` 0h ) ) )
21 13 20 eqtrd 
 |-  ( T e. LinOp -> ( T ` 0h ) = ( ( T ` 0h ) +h ( T ` 0h ) ) )
22 21 oveq1d 
 |-  ( T e. LinOp -> ( ( T ` 0h ) -h ( T ` 0h ) ) = ( ( ( T ` 0h ) +h ( T ` 0h ) ) -h ( T ` 0h ) ) )
23 hvsubid 
 |-  ( ( T ` 0h ) e. ~H -> ( ( T ` 0h ) -h ( T ` 0h ) ) = 0h )
24 17 23 syl 
 |-  ( T e. LinOp -> ( ( T ` 0h ) -h ( T ` 0h ) ) = 0h )
25 hvpncan 
 |-  ( ( ( T ` 0h ) e. ~H /\ ( T ` 0h ) e. ~H ) -> ( ( ( T ` 0h ) +h ( T ` 0h ) ) -h ( T ` 0h ) ) = ( T ` 0h ) )
26 25 anidms 
 |-  ( ( T ` 0h ) e. ~H -> ( ( ( T ` 0h ) +h ( T ` 0h ) ) -h ( T ` 0h ) ) = ( T ` 0h ) )
27 17 26 syl 
 |-  ( T e. LinOp -> ( ( ( T ` 0h ) +h ( T ` 0h ) ) -h ( T ` 0h ) ) = ( T ` 0h ) )
28 22 24 27 3eqtr3rd 
 |-  ( T e. LinOp -> ( T ` 0h ) = 0h )