Metamath Proof Explorer

Theorem lnfnsubi

Description: Subtraction property for a linear Hilbert space functional. (Contributed by NM, 13-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnfnl.1 
|- T e. LinFn
Assertion lnfnsubi 
|- ( ( 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 neg1cn 
 |-  -u 1 e. CC
3 1 lnfnaddmuli 
 |-  ( ( -u 1 e. CC /\ A e. ~H /\ B e. ~H ) -> ( T ` ( A +h ( -u 1 .h B ) ) ) = ( ( T ` A ) + ( -u 1 x. ( T ` B ) ) ) )
4 2 3 mp3an1 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A +h ( -u 1 .h B ) ) ) = ( ( T ` A ) + ( -u 1 x. ( T ` B ) ) ) )
5 hvsubval 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A -h B ) = ( A +h ( -u 1 .h B ) ) )
6 5 fveq2d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A -h B ) ) = ( T ` ( A +h ( -u 1 .h B ) ) ) )
7 1 lnfnfi 
 |-  T : ~H --> CC
8 7 ffvelcdmi 
 |-  ( A e. ~H -> ( T ` A ) e. CC )
9 7 ffvelcdmi 
 |-  ( B e. ~H -> ( T ` B ) e. CC )
10 mulm1 
 |-  ( ( T ` B ) e. CC -> ( -u 1 x. ( T ` B ) ) = -u ( T ` B ) )
11 10 oveq2d 
 |-  ( ( T ` B ) e. CC -> ( ( T ` A ) + ( -u 1 x. ( T ` B ) ) ) = ( ( T ` A ) + -u ( T ` B ) ) )
12 11 adantl 
 |-  ( ( ( T ` A ) e. CC /\ ( T ` B ) e. CC ) -> ( ( T ` A ) + ( -u 1 x. ( T ` B ) ) ) = ( ( T ` A ) + -u ( T ` B ) ) )
13 negsub 
 |-  ( ( ( T ` A ) e. CC /\ ( T ` B ) e. CC ) -> ( ( T ` A ) + -u ( T ` B ) ) = ( ( T ` A ) - ( T ` B ) ) )
14 12 13 eqtr2d 
 |-  ( ( ( T ` A ) e. CC /\ ( T ` B ) e. CC ) -> ( ( T ` A ) - ( T ` B ) ) = ( ( T ` A ) + ( -u 1 x. ( T ` B ) ) ) )
15 8 9 14 syl2an 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( T ` A ) - ( T ` B ) ) = ( ( T ` A ) + ( -u 1 x. ( T ` B ) ) ) )
16 4 6 15 3eqtr4d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( T ` ( A -h B ) ) = ( ( T ` A ) - ( T ` B ) ) )