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 syl5eqr ⊢ 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 ℎ