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

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 ⊢ 𝑇 ∈ LinFn
Assertion lnfnsubi ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) − ( 𝑇 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 lnfnl.1 ⊢ 𝑇 ∈ LinFn
2 neg1cn ⊢ - 1 ∈ ℂ
3 1 lnfnaddmuli ⊢ ( ( - 1 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( 𝑇 ‘ 𝐴 ) + ( - 1 · ( 𝑇 ‘ 𝐵 ) ) ) )
4 2 3 mp3an1 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( 𝑇 ‘ 𝐴 ) + ( - 1 · ( 𝑇 ‘ 𝐵 ) ) ) )
5 hvsubval ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
6 5 fveq2d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( 𝑇 ‘ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) )
7 1 lnfnfi ⊢ 𝑇 : ℋ ⟶ ℂ
8 7 ffvelcdmi ⊢ ( 𝐴 ∈ ℋ → ( 𝑇 ‘ 𝐴 ) ∈ ℂ )
9 7 ffvelcdmi ⊢ ( 𝐵 ∈ ℋ → ( 𝑇 ‘ 𝐵 ) ∈ ℂ )
10 mulm1 ⊢ ( ( 𝑇 ‘ 𝐵 ) ∈ ℂ → ( - 1 · ( 𝑇 ‘ 𝐵 ) ) = - ( 𝑇 ‘ 𝐵 ) )
11 10 oveq2d ⊢ ( ( 𝑇 ‘ 𝐵 ) ∈ ℂ → ( ( 𝑇 ‘ 𝐴 ) + ( - 1 · ( 𝑇 ‘ 𝐵 ) ) ) = ( ( 𝑇 ‘ 𝐴 ) + - ( 𝑇 ‘ 𝐵 ) ) )
12 11 adantl ⊢ ( ( ( 𝑇 ‘ 𝐴 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝐵 ) ∈ ℂ ) → ( ( 𝑇 ‘ 𝐴 ) + ( - 1 · ( 𝑇 ‘ 𝐵 ) ) ) = ( ( 𝑇 ‘ 𝐴 ) + - ( 𝑇 ‘ 𝐵 ) ) )
13 negsub ⊢ ( ( ( 𝑇 ‘ 𝐴 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝐵 ) ∈ ℂ ) → ( ( 𝑇 ‘ 𝐴 ) + - ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) − ( 𝑇 ‘ 𝐵 ) ) )
14 12 13 eqtr2d ⊢ ( ( ( 𝑇 ‘ 𝐴 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝐵 ) ∈ ℂ ) → ( ( 𝑇 ‘ 𝐴 ) − ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) + ( - 1 · ( 𝑇 ‘ 𝐵 ) ) ) )
15 8 9 14 syl2an ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) − ( 𝑇 ‘ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) + ( - 1 · ( 𝑇 ‘ 𝐵 ) ) ) )
16 4 6 15 3eqtr4d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑇 ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( 𝑇 ‘ 𝐴 ) − ( 𝑇 ‘ 𝐵 ) ) )