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 ∈ LinFn
Assertion lnfnsubi ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A - ℎ B = T ⁡ A − T ⁡ B

Proof

Step Hyp Ref Expression
1 lnfnl.1 ⊢ T ∈ LinFn
2 neg1cn ⊢ − 1 ∈ ℂ
3 1 lnfnaddmuli ⊢ − 1 ∈ ℂ ∧ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A + ℎ -1 ⋅ ℎ B = T ⁡ A + -1 ⁢ T ⁡ B
4 2 3 mp3an1 ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A + ℎ -1 ⋅ ℎ B = T ⁡ A + -1 ⁢ T ⁡ B
5 hvsubval ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ B = A + ℎ -1 ⋅ ℎ B
6 5 fveq2d ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A - ℎ B = T ⁡ A + ℎ -1 ⋅ ℎ B
7 1 lnfnfi ⊢ T : ℋ ⟶ ℂ
8 7 ffvelcdmi ⊢ A ∈ ℋ → T ⁡ A ∈ ℂ
9 7 ffvelcdmi ⊢ B ∈ ℋ → T ⁡ B ∈ ℂ
10 mulm1 ⊢ T ⁡ B ∈ ℂ → -1 ⁢ T ⁡ B = − T ⁡ B
11 10 oveq2d ⊢ T ⁡ B ∈ ℂ → T ⁡ A + -1 ⁢ T ⁡ B = T ⁡ A + − T ⁡ B
12 11 adantl ⊢ T ⁡ A ∈ ℂ ∧ T ⁡ B ∈ ℂ → T ⁡ A + -1 ⁢ T ⁡ B = T ⁡ A + − T ⁡ B
13 negsub ⊢ T ⁡ A ∈ ℂ ∧ T ⁡ B ∈ ℂ → T ⁡ A + − T ⁡ B = T ⁡ A − T ⁡ B
14 12 13 eqtr2d ⊢ T ⁡ A ∈ ℂ ∧ T ⁡ B ∈ ℂ → T ⁡ A − T ⁡ B = T ⁡ A + -1 ⁢ T ⁡ B
15 8 9 14 syl2an ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A − T ⁡ B = T ⁡ A + -1 ⁢ T ⁡ B
16 4 6 15 3eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A - ℎ B = T ⁡ A − T ⁡ B