# 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}\in \mathrm{LinFn}$
Assertion lnfn0i ${⊢}{T}\left({0}_{ℎ}\right)=0$

### Proof

Step Hyp Ref Expression
1 lnfnl.1 ${⊢}{T}\in \mathrm{LinFn}$
2 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
3 1 lnfnfi ${⊢}{T}:ℋ⟶ℂ$
4 3 ffvelrni ${⊢}{0}_{ℎ}\in ℋ\to {T}\left({0}_{ℎ}\right)\in ℂ$
5 2 4 ax-mp ${⊢}{T}\left({0}_{ℎ}\right)\in ℂ$
6 5 5 pncan3oi ${⊢}{T}\left({0}_{ℎ}\right)+{T}\left({0}_{ℎ}\right)-{T}\left({0}_{ℎ}\right)={T}\left({0}_{ℎ}\right)$
7 ax-1cn ${⊢}1\in ℂ$
8 1 lnfnli ${⊢}\left(1\in ℂ\wedge {0}_{ℎ}\in ℋ\wedge {0}_{ℎ}\in ℋ\right)\to {T}\left(\left(1{\cdot }_{ℎ}{0}_{ℎ}\right){+}_{ℎ}{0}_{ℎ}\right)=1{T}\left({0}_{ℎ}\right)+{T}\left({0}_{ℎ}\right)$
9 7 2 2 8 mp3an ${⊢}{T}\left(\left(1{\cdot }_{ℎ}{0}_{ℎ}\right){+}_{ℎ}{0}_{ℎ}\right)=1{T}\left({0}_{ℎ}\right)+{T}\left({0}_{ℎ}\right)$
10 7 2 hvmulcli ${⊢}1{\cdot }_{ℎ}{0}_{ℎ}\in ℋ$
11 ax-hvaddid ${⊢}1{\cdot }_{ℎ}{0}_{ℎ}\in ℋ\to \left(1{\cdot }_{ℎ}{0}_{ℎ}\right){+}_{ℎ}{0}_{ℎ}=1{\cdot }_{ℎ}{0}_{ℎ}$
12 10 11 ax-mp ${⊢}\left(1{\cdot }_{ℎ}{0}_{ℎ}\right){+}_{ℎ}{0}_{ℎ}=1{\cdot }_{ℎ}{0}_{ℎ}$
13 ax-hvmulid ${⊢}{0}_{ℎ}\in ℋ\to 1{\cdot }_{ℎ}{0}_{ℎ}={0}_{ℎ}$
14 2 13 ax-mp ${⊢}1{\cdot }_{ℎ}{0}_{ℎ}={0}_{ℎ}$
15 12 14 eqtri ${⊢}\left(1{\cdot }_{ℎ}{0}_{ℎ}\right){+}_{ℎ}{0}_{ℎ}={0}_{ℎ}$
16 15 fveq2i ${⊢}{T}\left(\left(1{\cdot }_{ℎ}{0}_{ℎ}\right){+}_{ℎ}{0}_{ℎ}\right)={T}\left({0}_{ℎ}\right)$
17 9 16 eqtr3i ${⊢}1{T}\left({0}_{ℎ}\right)+{T}\left({0}_{ℎ}\right)={T}\left({0}_{ℎ}\right)$
18 5 mulid2i ${⊢}1{T}\left({0}_{ℎ}\right)={T}\left({0}_{ℎ}\right)$
19 18 oveq1i ${⊢}1{T}\left({0}_{ℎ}\right)+{T}\left({0}_{ℎ}\right)={T}\left({0}_{ℎ}\right)+{T}\left({0}_{ℎ}\right)$
20 17 19 eqtr3i ${⊢}{T}\left({0}_{ℎ}\right)={T}\left({0}_{ℎ}\right)+{T}\left({0}_{ℎ}\right)$
21 20 oveq1i ${⊢}{T}\left({0}_{ℎ}\right)-{T}\left({0}_{ℎ}\right)={T}\left({0}_{ℎ}\right)+{T}\left({0}_{ℎ}\right)-{T}\left({0}_{ℎ}\right)$
22 5 subidi ${⊢}{T}\left({0}_{ℎ}\right)-{T}\left({0}_{ℎ}\right)=0$
23 21 22 eqtr3i ${⊢}{T}\left({0}_{ℎ}\right)+{T}\left({0}_{ℎ}\right)-{T}\left({0}_{ℎ}\right)=0$
24 6 23 eqtr3i ${⊢}{T}\left({0}_{ℎ}\right)=0$