Metamath Proof Explorer

Theorem lnfn0i

Description: The value of a linear Hilbert space functional at zero is zero. Remark in Beran p. 99. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnfnl.1 ⊢ T ∈ LinFn
Assertion lnfn0i ⊢ T ⁡ 0 ℎ = 0

Proof

Step Hyp Ref Expression
1 lnfnl.1 ⊢ T ∈ LinFn
2 ax-hv0cl ⊢ 0 ℎ ∈ ℋ
3 1 lnfnfi ⊢ T : ℋ ⟶ ℂ
4 3 ffvelrni ⊢ 0 ℎ ∈ ℋ → T ⁡ 0 ℎ ∈ ℂ
5 2 4 ax-mp ⊢ T ⁡ 0 ℎ ∈ ℂ
6 5 5 pncan3oi ⊢ T ⁡ 0 ℎ + T ⁡ 0 ℎ - T ⁡ 0 ℎ = T ⁡ 0 ℎ
7 ax-1cn ⊢ 1 ∈ ℂ
8 1 lnfnli ⊢ 1 ∈ ℂ ∧ 0 ℎ ∈ ℋ ∧ 0 ℎ ∈ ℋ → T ⁡ 1 ⋅ ℎ 0 ℎ + ℎ 0 ℎ = 1 ⁢ T ⁡ 0 ℎ + T ⁡ 0 ℎ
9 7 2 2 8 mp3an ⊢ T ⁡ 1 ⋅ ℎ 0 ℎ + ℎ 0 ℎ = 1 ⁢ T ⁡ 0 ℎ + T ⁡ 0 ℎ
10 7 2 hvmulcli ⊢ 1 ⋅ ℎ 0 ℎ ∈ ℋ
11 ax-hvaddid ⊢ 1 ⋅ ℎ 0 ℎ ∈ ℋ → 1 ⋅ ℎ 0 ℎ + ℎ 0 ℎ = 1 ⋅ ℎ 0 ℎ
12 10 11 ax-mp ⊢ 1 ⋅ ℎ 0 ℎ + ℎ 0 ℎ = 1 ⋅ ℎ 0 ℎ
13 ax-hvmulid ⊢ 0 ℎ ∈ ℋ → 1 ⋅ ℎ 0 ℎ = 0 ℎ
14 2 13 ax-mp ⊢ 1 ⋅ ℎ 0 ℎ = 0 ℎ
15 12 14 eqtri ⊢ 1 ⋅ ℎ 0 ℎ + ℎ 0 ℎ = 0 ℎ
16 15 fveq2i ⊢ T ⁡ 1 ⋅ ℎ 0 ℎ + ℎ 0 ℎ = T ⁡ 0 ℎ
17 9 16 eqtr3i ⊢ 1 ⁢ T ⁡ 0 ℎ + T ⁡ 0 ℎ = T ⁡ 0 ℎ
18 5 mulid2i ⊢ 1 ⁢ T ⁡ 0 ℎ = T ⁡ 0 ℎ
19 18 oveq1i ⊢ 1 ⁢ T ⁡ 0 ℎ + T ⁡ 0 ℎ = T ⁡ 0 ℎ + T ⁡ 0 ℎ
20 17 19 eqtr3i ⊢ T ⁡ 0 ℎ = T ⁡ 0 ℎ + T ⁡ 0 ℎ
21 20 oveq1i ⊢ T ⁡ 0 ℎ − T ⁡ 0 ℎ = T ⁡ 0 ℎ + T ⁡ 0 ℎ - T ⁡ 0 ℎ
22 5 subidi ⊢ T ⁡ 0 ℎ − T ⁡ 0 ℎ = 0
23 21 22 eqtr3i ⊢ T ⁡ 0 ℎ + T ⁡ 0 ℎ - T ⁡ 0 ℎ = 0
24 6 23 eqtr3i ⊢ T ⁡ 0 ℎ = 0