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 LinOp T 0 = 0

Proof

Step Hyp Ref Expression
1 ax-1cn 1
2 ax-hv0cl 0
3 1 2 hvmulcli 1 0
4 ax-hvaddid 1 0 1 0 + 0 = 1 0
5 3 4 ax-mp 1 0 + 0 = 1 0
6 ax-hvmulid 0 1 0 = 0
7 2 6 ax-mp 1 0 = 0
8 5 7 eqtri 1 0 + 0 = 0
9 8 fveq2i T 1 0 + 0 = T 0
10 lnopl T LinOp 1 0 0 T 1 0 + 0 = 1 T 0 + T 0
11 2 2 10 mpanr12 T LinOp 1 T 1 0 + 0 = 1 T 0 + T 0
12 1 11 mpan2 T LinOp T 1 0 + 0 = 1 T 0 + T 0
13 9 12 eqtr3id T LinOp T 0 = 1 T 0 + T 0
14 lnopf T LinOp T :
15 ffvelrn T : 0 T 0
16 2 15 mpan2 T : T 0
17 14 16 syl T LinOp T 0
18 ax-hvmulid T 0 1 T 0 = T 0
19 17 18 syl T LinOp 1 T 0 = T 0
20 19 oveq1d T LinOp 1 T 0 + T 0 = T 0 + T 0
21 13 20 eqtrd T LinOp T 0 = T 0 + T 0
22 21 oveq1d T LinOp T 0 - T 0 = T 0 + T 0 - T 0
23 hvsubid T 0 T 0 - T 0 = 0
24 17 23 syl T LinOp T 0 - T 0 = 0
25 hvpncan T 0 T 0 T 0 + T 0 - T 0 = T 0
26 25 anidms T 0 T 0 + T 0 - T 0 = T 0
27 17 26 syl T LinOp T 0 + T 0 - T 0 = T 0
28 22 24 27 3eqtr3rd T LinOp T 0 = 0