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 TLinOpT0=0

Proof

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