# Metamath Proof Explorer

## Theorem lnop0

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

Ref Expression
Assertion lnop0 ${⊢}{T}\in \mathrm{LinOp}\to {T}\left({0}_{ℎ}\right)={0}_{ℎ}$

### Proof

Step Hyp Ref Expression
1 ax-1cn ${⊢}1\in ℂ$
2 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
3 1 2 hvmulcli ${⊢}1{\cdot }_{ℎ}{0}_{ℎ}\in ℋ$
4 ax-hvaddid ${⊢}1{\cdot }_{ℎ}{0}_{ℎ}\in ℋ\to \left(1{\cdot }_{ℎ}{0}_{ℎ}\right){+}_{ℎ}{0}_{ℎ}=1{\cdot }_{ℎ}{0}_{ℎ}$
5 3 4 ax-mp ${⊢}\left(1{\cdot }_{ℎ}{0}_{ℎ}\right){+}_{ℎ}{0}_{ℎ}=1{\cdot }_{ℎ}{0}_{ℎ}$
6 ax-hvmulid ${⊢}{0}_{ℎ}\in ℋ\to 1{\cdot }_{ℎ}{0}_{ℎ}={0}_{ℎ}$
7 2 6 ax-mp ${⊢}1{\cdot }_{ℎ}{0}_{ℎ}={0}_{ℎ}$
8 5 7 eqtri ${⊢}\left(1{\cdot }_{ℎ}{0}_{ℎ}\right){+}_{ℎ}{0}_{ℎ}={0}_{ℎ}$
9 8 fveq2i ${⊢}{T}\left(\left(1{\cdot }_{ℎ}{0}_{ℎ}\right){+}_{ℎ}{0}_{ℎ}\right)={T}\left({0}_{ℎ}\right)$
10 lnopl ${⊢}\left(\left({T}\in \mathrm{LinOp}\wedge 1\in ℂ\right)\wedge \left({0}_{ℎ}\in ℋ\wedge {0}_{ℎ}\in ℋ\right)\right)\to {T}\left(\left(1{\cdot }_{ℎ}{0}_{ℎ}\right){+}_{ℎ}{0}_{ℎ}\right)=\left(1{\cdot }_{ℎ}{T}\left({0}_{ℎ}\right)\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)$
11 2 2 10 mpanr12 ${⊢}\left({T}\in \mathrm{LinOp}\wedge 1\in ℂ\right)\to {T}\left(\left(1{\cdot }_{ℎ}{0}_{ℎ}\right){+}_{ℎ}{0}_{ℎ}\right)=\left(1{\cdot }_{ℎ}{T}\left({0}_{ℎ}\right)\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)$
12 1 11 mpan2 ${⊢}{T}\in \mathrm{LinOp}\to {T}\left(\left(1{\cdot }_{ℎ}{0}_{ℎ}\right){+}_{ℎ}{0}_{ℎ}\right)=\left(1{\cdot }_{ℎ}{T}\left({0}_{ℎ}\right)\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)$
13 9 12 syl5eqr ${⊢}{T}\in \mathrm{LinOp}\to {T}\left({0}_{ℎ}\right)=\left(1{\cdot }_{ℎ}{T}\left({0}_{ℎ}\right)\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)$
14 lnopf ${⊢}{T}\in \mathrm{LinOp}\to {T}:ℋ⟶ℋ$
15 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {0}_{ℎ}\in ℋ\right)\to {T}\left({0}_{ℎ}\right)\in ℋ$
16 2 15 mpan2 ${⊢}{T}:ℋ⟶ℋ\to {T}\left({0}_{ℎ}\right)\in ℋ$
17 14 16 syl ${⊢}{T}\in \mathrm{LinOp}\to {T}\left({0}_{ℎ}\right)\in ℋ$
18 ax-hvmulid ${⊢}{T}\left({0}_{ℎ}\right)\in ℋ\to 1{\cdot }_{ℎ}{T}\left({0}_{ℎ}\right)={T}\left({0}_{ℎ}\right)$
19 17 18 syl ${⊢}{T}\in \mathrm{LinOp}\to 1{\cdot }_{ℎ}{T}\left({0}_{ℎ}\right)={T}\left({0}_{ℎ}\right)$
20 19 oveq1d ${⊢}{T}\in \mathrm{LinOp}\to \left(1{\cdot }_{ℎ}{T}\left({0}_{ℎ}\right)\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)={T}\left({0}_{ℎ}\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)$
21 13 20 eqtrd ${⊢}{T}\in \mathrm{LinOp}\to {T}\left({0}_{ℎ}\right)={T}\left({0}_{ℎ}\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)$
22 21 oveq1d ${⊢}{T}\in \mathrm{LinOp}\to {T}\left({0}_{ℎ}\right){-}_{ℎ}{T}\left({0}_{ℎ}\right)=\left({T}\left({0}_{ℎ}\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)\right){-}_{ℎ}{T}\left({0}_{ℎ}\right)$
23 hvsubid ${⊢}{T}\left({0}_{ℎ}\right)\in ℋ\to {T}\left({0}_{ℎ}\right){-}_{ℎ}{T}\left({0}_{ℎ}\right)={0}_{ℎ}$
24 17 23 syl ${⊢}{T}\in \mathrm{LinOp}\to {T}\left({0}_{ℎ}\right){-}_{ℎ}{T}\left({0}_{ℎ}\right)={0}_{ℎ}$
25 hvpncan ${⊢}\left({T}\left({0}_{ℎ}\right)\in ℋ\wedge {T}\left({0}_{ℎ}\right)\in ℋ\right)\to \left({T}\left({0}_{ℎ}\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)\right){-}_{ℎ}{T}\left({0}_{ℎ}\right)={T}\left({0}_{ℎ}\right)$
26 25 anidms ${⊢}{T}\left({0}_{ℎ}\right)\in ℋ\to \left({T}\left({0}_{ℎ}\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)\right){-}_{ℎ}{T}\left({0}_{ℎ}\right)={T}\left({0}_{ℎ}\right)$
27 17 26 syl ${⊢}{T}\in \mathrm{LinOp}\to \left({T}\left({0}_{ℎ}\right){+}_{ℎ}{T}\left({0}_{ℎ}\right)\right){-}_{ℎ}{T}\left({0}_{ℎ}\right)={T}\left({0}_{ℎ}\right)$
28 22 24 27 3eqtr3rd ${⊢}{T}\in \mathrm{LinOp}\to {T}\left({0}_{ℎ}\right)={0}_{ℎ}$