# Metamath Proof Explorer

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`
`|- ( ( 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 ) ) )`
` |-  ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( ( 1 .h A ) +h B ) ) = ( T ` ( A +h B ) ) )`
8 1 lnopfi
` |-  T : ~H --> ~H`
9 8 ffvelrni
` |-  ( 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 ) )`
` |-  ( ( A e. ~H /\ B e. ~H ) -> ( 1 .h ( T ` A ) ) = ( T ` A ) )`
` |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( 1 .h ( T ` A ) ) +h ( T ` B ) ) = ( ( T ` A ) +h ( T ` B ) ) )`
` |-  ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A +h B ) ) = ( ( T ` A ) +h ( T ` B ) ) )`