This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lnfn0i

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

Ref Expression
Hypothesis lnfnl.1 ⊢ 𝑇 ∈ LinFn
Assertion lnfn0i ( 𝑇 ‘ 0ℎ ) = 0

Proof

Step Hyp Ref Expression
1 lnfnl.1 ⊢ 𝑇 ∈ LinFn
2 ax-hv0cl ⊢ 0ℎ ∈ ℋ
3 1 lnfnfi ⊢ 𝑇 : ℋ ⟶ ℂ
4 3 ffvelcdmi ⊢ ( 0ℎ ∈ ℋ → ( 𝑇 ‘ 0ℎ ) ∈ ℂ )
5 2 4 ax-mp ⊢ ( 𝑇 ‘ 0ℎ ) ∈ ℂ
6 5 5 pncan3oi ⊢ ( ( ( 𝑇 ‘ 0ℎ ) + ( 𝑇 ‘ 0ℎ ) ) − ( 𝑇 ‘ 0ℎ ) ) = ( 𝑇 ‘ 0ℎ )
7 ax-1cn ⊢ 1 ∈ ℂ
8 1 lnfnli ⊢ ( ( 1 ∈ ℂ ∧ 0ℎ ∈ ℋ ∧ 0ℎ ∈ ℋ ) → ( 𝑇 ‘ ( ( 1 ·ℎ 0ℎ ) +ℎ 0ℎ ) ) = ( ( 1 · ( 𝑇 ‘ 0ℎ ) ) + ( 𝑇 ‘ 0ℎ ) ) )
9 7 2 2 8 mp3an ⊢ ( 𝑇 ‘ ( ( 1 ·ℎ 0ℎ ) +ℎ 0ℎ ) ) = ( ( 1 · ( 𝑇 ‘ 0ℎ ) ) + ( 𝑇 ‘ 0ℎ ) )
10 7 2 hvmulcli ⊢ ( 1 ·ℎ 0ℎ ) ∈ ℋ
11 ax-hvaddid ⊢ ( ( 1 ·ℎ 0ℎ ) ∈ ℋ → ( ( 1 ·ℎ 0ℎ ) +ℎ 0ℎ ) = ( 1 ·ℎ 0ℎ ) )
12 10 11 ax-mp ⊢ ( ( 1 ·ℎ 0ℎ ) +ℎ 0ℎ ) = ( 1 ·ℎ 0ℎ )
13 ax-hvmulid ⊢ ( 0ℎ ∈ ℋ → ( 1 ·ℎ 0ℎ ) = 0ℎ )
14 2 13 ax-mp ⊢ ( 1 ·ℎ 0ℎ ) = 0ℎ
15 12 14 eqtri ⊢ ( ( 1 ·ℎ 0ℎ ) +ℎ 0ℎ ) = 0ℎ
16 15 fveq2i ⊢ ( 𝑇 ‘ ( ( 1 ·ℎ 0ℎ ) +ℎ 0ℎ ) ) = ( 𝑇 ‘ 0ℎ )
17 9 16 eqtr3i ⊢ ( ( 1 · ( 𝑇 ‘ 0ℎ ) ) + ( 𝑇 ‘ 0ℎ ) ) = ( 𝑇 ‘ 0ℎ )
18 5 mullidi ⊢ ( 1 · ( 𝑇 ‘ 0ℎ ) ) = ( 𝑇 ‘ 0ℎ )
19 18 oveq1i ⊢ ( ( 1 · ( 𝑇 ‘ 0ℎ ) ) + ( 𝑇 ‘ 0ℎ ) ) = ( ( 𝑇 ‘ 0ℎ ) + ( 𝑇 ‘ 0ℎ ) )
20 17 19 eqtr3i ⊢ ( 𝑇 ‘ 0ℎ ) = ( ( 𝑇 ‘ 0ℎ ) + ( 𝑇 ‘ 0ℎ ) )
21 20 oveq1i ⊢ ( ( 𝑇 ‘ 0ℎ ) − ( 𝑇 ‘ 0ℎ ) ) = ( ( ( 𝑇 ‘ 0ℎ ) + ( 𝑇 ‘ 0ℎ ) ) − ( 𝑇 ‘ 0ℎ ) )
22 5 subidi ⊢ ( ( 𝑇 ‘ 0ℎ ) − ( 𝑇 ‘ 0ℎ ) ) = 0
23 21 22 eqtr3i ⊢ ( ( ( 𝑇 ‘ 0ℎ ) + ( 𝑇 ‘ 0ℎ ) ) − ( 𝑇 ‘ 0ℎ ) ) = 0
24 6 23 eqtr3i ⊢ ( 𝑇 ‘ 0ℎ ) = 0