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 ( 𝑇 ∈ LinOp → ( 𝑇 ‘ 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 ⊢ ( 𝑇 ‘ ( ( 1 ·ℎ 0ℎ ) +ℎ 0ℎ ) ) = ( 𝑇 ‘ 0ℎ )
10 lnopl ⊢ ( ( ( 𝑇 ∈ LinOp ∧ 1 ∈ ℂ ) ∧ ( 0ℎ ∈ ℋ ∧ 0ℎ ∈ ℋ ) ) → ( 𝑇 ‘ ( ( 1 ·ℎ 0ℎ ) +ℎ 0ℎ ) ) = ( ( 1 ·ℎ ( 𝑇 ‘ 0ℎ ) ) +ℎ ( 𝑇 ‘ 0ℎ ) ) )
11 2 2 10 mpanr12 ⊢ ( ( 𝑇 ∈ LinOp ∧ 1 ∈ ℂ ) → ( 𝑇 ‘ ( ( 1 ·ℎ 0ℎ ) +ℎ 0ℎ ) ) = ( ( 1 ·ℎ ( 𝑇 ‘ 0ℎ ) ) +ℎ ( 𝑇 ‘ 0ℎ ) ) )
12 1 11 mpan2 ⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ‘ ( ( 1 ·ℎ 0ℎ ) +ℎ 0ℎ ) ) = ( ( 1 ·ℎ ( 𝑇 ‘ 0ℎ ) ) +ℎ ( 𝑇 ‘ 0ℎ ) ) )
13 9 12 eqtr3id ⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ‘ 0ℎ ) = ( ( 1 ·ℎ ( 𝑇 ‘ 0ℎ ) ) +ℎ ( 𝑇 ‘ 0ℎ ) ) )
14 lnopf ⊢ ( 𝑇 ∈ LinOp → 𝑇 : ℋ ⟶ ℋ )
15 ffvelrn ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 0ℎ ∈ ℋ ) → ( 𝑇 ‘ 0ℎ ) ∈ ℋ )
16 2 15 mpan2 ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 ‘ 0ℎ ) ∈ ℋ )
17 14 16 syl ⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ‘ 0ℎ ) ∈ ℋ )
18 ax-hvmulid ⊢ ( ( 𝑇 ‘ 0ℎ ) ∈ ℋ → ( 1 ·ℎ ( 𝑇 ‘ 0ℎ ) ) = ( 𝑇 ‘ 0ℎ ) )
19 17 18 syl ⊢ ( 𝑇 ∈ LinOp → ( 1 ·ℎ ( 𝑇 ‘ 0ℎ ) ) = ( 𝑇 ‘ 0ℎ ) )
20 19 oveq1d ⊢ ( 𝑇 ∈ LinOp → ( ( 1 ·ℎ ( 𝑇 ‘ 0ℎ ) ) +ℎ ( 𝑇 ‘ 0ℎ ) ) = ( ( 𝑇 ‘ 0ℎ ) +ℎ ( 𝑇 ‘ 0ℎ ) ) )
21 13 20 eqtrd ⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ‘ 0ℎ ) = ( ( 𝑇 ‘ 0ℎ ) +ℎ ( 𝑇 ‘ 0ℎ ) ) )
22 21 oveq1d ⊢ ( 𝑇 ∈ LinOp → ( ( 𝑇 ‘ 0ℎ ) −ℎ ( 𝑇 ‘ 0ℎ ) ) = ( ( ( 𝑇 ‘ 0ℎ ) +ℎ ( 𝑇 ‘ 0ℎ ) ) −ℎ ( 𝑇 ‘ 0ℎ ) ) )
23 hvsubid ⊢ ( ( 𝑇 ‘ 0ℎ ) ∈ ℋ → ( ( 𝑇 ‘ 0ℎ ) −ℎ ( 𝑇 ‘ 0ℎ ) ) = 0ℎ )
24 17 23 syl ⊢ ( 𝑇 ∈ LinOp → ( ( 𝑇 ‘ 0ℎ ) −ℎ ( 𝑇 ‘ 0ℎ ) ) = 0ℎ )
25 hvpncan ⊢ ( ( ( 𝑇 ‘ 0ℎ ) ∈ ℋ ∧ ( 𝑇 ‘ 0ℎ ) ∈ ℋ ) → ( ( ( 𝑇 ‘ 0ℎ ) +ℎ ( 𝑇 ‘ 0ℎ ) ) −ℎ ( 𝑇 ‘ 0ℎ ) ) = ( 𝑇 ‘ 0ℎ ) )
26 25 anidms ⊢ ( ( 𝑇 ‘ 0ℎ ) ∈ ℋ → ( ( ( 𝑇 ‘ 0ℎ ) +ℎ ( 𝑇 ‘ 0ℎ ) ) −ℎ ( 𝑇 ‘ 0ℎ ) ) = ( 𝑇 ‘ 0ℎ ) )
27 17 26 syl ⊢ ( 𝑇 ∈ LinOp → ( ( ( 𝑇 ‘ 0ℎ ) +ℎ ( 𝑇 ‘ 0ℎ ) ) −ℎ ( 𝑇 ‘ 0ℎ ) ) = ( 𝑇 ‘ 0ℎ ) )
28 22 24 27 3eqtr3rd ⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ‘ 0ℎ ) = 0ℎ )