Metamath Proof Explorer

Theorem lnfnaddi

Description: Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnfnl.1 
|- T e. LinFn
Assertion lnfnaddi 
|- ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A +h B ) ) = ( ( T ` A ) + ( T ` B ) ) )

Proof

Step Hyp Ref Expression
1 lnfnl.1 
 |-  T e. LinFn
2 ax-1cn 
 |-  1 e. CC
3 1 lnfnli 
 |-  ( ( 1 e. CC /\ A e. ~H /\ B e. ~H ) -> ( T ` ( ( 1 .h A ) +h B ) ) = ( ( 1 x. ( T ` A ) ) + ( T ` B ) ) )
4 2 3 mp3an1 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( ( 1 .h A ) +h B ) ) = ( ( 1 x. ( T ` A ) ) + ( T ` B ) ) )
5 ax-hvmulid 
 |-  ( A e. ~H -> ( 1 .h A ) = A )
6 5 fvoveq1d 
 |-  ( A e. ~H -> ( T ` ( ( 1 .h A ) +h B ) ) = ( T ` ( A +h B ) ) )
7 6 adantr 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( ( 1 .h A ) +h B ) ) = ( T ` ( A +h B ) ) )
8 1 lnfnfi 
 |-  T : ~H --> CC
9 8 ffvelrni 
 |-  ( A e. ~H -> ( T ` A ) e. CC )
10 9 mulid2d 
 |-  ( A e. ~H -> ( 1 x. ( T ` A ) ) = ( T ` A ) )
11 10 adantr 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( 1 x. ( T ` A ) ) = ( T ` A ) )
12 11 oveq1d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( 1 x. ( T ` A ) ) + ( T ` B ) ) = ( ( T ` A ) + ( T ` B ) ) )
13 4 7 12 3eqtr3d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A +h B ) ) = ( ( T ` A ) + ( T ` B ) ) )