Metamath Proof Explorer

Theorem lnopaddi

Description: Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005) (New usage is discouraged.)

Ref Expression
Hypothesis lnopl.1 
|- T e. LinOp
Assertion lnopaddi 
|- ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A +h B ) ) = ( ( T ` A ) +h ( T ` B ) ) )

Proof

Step Hyp Ref Expression
1 lnopl.1 
 |-  T e. LinOp
2 ax-1cn 
 |-  1 e. CC
3 1 lnopli 
 |-  ( ( 1 e. CC /\ A e. ~H /\ B e. ~H ) -> ( T ` ( ( 1 .h A ) +h B ) ) = ( ( 1 .h ( T ` A ) ) +h ( T ` B ) ) )
4 2 3 mp3an1 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( ( 1 .h A ) +h B ) ) = ( ( 1 .h ( T ` A ) ) +h ( 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 lnopfi 
 |-  T : ~H --> ~H
9 8 ffvelcdmi 
 |-  ( A e. ~H -> ( T ` A ) e. ~H )
10 ax-hvmulid 
 |-  ( ( T ` A ) e. ~H -> ( 1 .h ( T ` A ) ) = ( T ` A ) )
11 9 10 syl 
 |-  ( A e. ~H -> ( 1 .h ( T ` A ) ) = ( T ` A ) )
12 11 adantr 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( 1 .h ( T ` A ) ) = ( T ` A ) )
13 12 oveq1d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( 1 .h ( T ` A ) ) +h ( T ` B ) ) = ( ( T ` A ) +h ( T ` B ) ) )
14 4 7 13 3eqtr3d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A +h B ) ) = ( ( T ` A ) +h ( T ` B ) ) )