This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lnfn0i

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

Ref Expression
Hypothesis lnfnl.1 
|- T e. LinFn
Assertion lnfn0i 
|- ( T ` 0h ) = 0

Proof

Step Hyp Ref Expression
1 lnfnl.1 
 |-  T e. LinFn
2 ax-hv0cl 
 |-  0h e. ~H
3 1 lnfnfi 
 |-  T : ~H --> CC
4 3 ffvelcdmi 
 |-  ( 0h e. ~H -> ( T ` 0h ) e. CC )
5 2 4 ax-mp 
 |-  ( T ` 0h ) e. CC
6 5 5 pncan3oi 
 |-  ( ( ( T ` 0h ) + ( T ` 0h ) ) - ( T ` 0h ) ) = ( T ` 0h )
7 ax-1cn 
 |-  1 e. CC
8 1 lnfnli 
 |-  ( ( 1 e. CC /\ 0h e. ~H /\ 0h e. ~H ) -> ( T ` ( ( 1 .h 0h ) +h 0h ) ) = ( ( 1 x. ( T ` 0h ) ) + ( T ` 0h ) ) )
9 7 2 2 8 mp3an 
 |-  ( T ` ( ( 1 .h 0h ) +h 0h ) ) = ( ( 1 x. ( T ` 0h ) ) + ( T ` 0h ) )
10 7 2 hvmulcli 
 |-  ( 1 .h 0h ) e. ~H
11 ax-hvaddid 
 |-  ( ( 1 .h 0h ) e. ~H -> ( ( 1 .h 0h ) +h 0h ) = ( 1 .h 0h ) )
12 10 11 ax-mp 
 |-  ( ( 1 .h 0h ) +h 0h ) = ( 1 .h 0h )
13 ax-hvmulid 
 |-  ( 0h e. ~H -> ( 1 .h 0h ) = 0h )
14 2 13 ax-mp 
 |-  ( 1 .h 0h ) = 0h
15 12 14 eqtri 
 |-  ( ( 1 .h 0h ) +h 0h ) = 0h
16 15 fveq2i 
 |-  ( T ` ( ( 1 .h 0h ) +h 0h ) ) = ( T ` 0h )
17 9 16 eqtr3i 
 |-  ( ( 1 x. ( T ` 0h ) ) + ( T ` 0h ) ) = ( T ` 0h )
18 5 mullidi 
 |-  ( 1 x. ( T ` 0h ) ) = ( T ` 0h )
19 18 oveq1i 
 |-  ( ( 1 x. ( T ` 0h ) ) + ( T ` 0h ) ) = ( ( T ` 0h ) + ( T ` 0h ) )
20 17 19 eqtr3i 
 |-  ( T ` 0h ) = ( ( T ` 0h ) + ( T ` 0h ) )
21 20 oveq1i 
 |-  ( ( T ` 0h ) - ( T ` 0h ) ) = ( ( ( T ` 0h ) + ( T ` 0h ) ) - ( T ` 0h ) )
22 5 subidi 
 |-  ( ( T ` 0h ) - ( T ` 0h ) ) = 0
23 21 22 eqtr3i 
 |-  ( ( ( T ` 0h ) + ( T ` 0h ) ) - ( T ` 0h ) ) = 0
24 6 23 eqtr3i 
 |-  ( T ` 0h ) = 0