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

Metamath Proof Explorer

Theorem 0lnfn

Description: The identically zero function is a linear Hilbert space functional. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion 0lnfn ( ℋ × { 0 } ) ∈ LinFn

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 1 fconst6 ⊢ ( ℋ × { 0 } ) : ℋ ⟶ ℂ
3 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ )
4 hvaddcl ⊢ ( ( ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ )
5 3 4 sylan ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ )
6 c0ex ⊢ 0 ∈ V
7 6 fvconst2 ⊢ ( ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ∈ ℋ → ( ( ℋ × { 0 } ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = 0 )
8 5 7 syl ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( ℋ × { 0 } ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = 0 )
9 6 fvconst2 ⊢ ( 𝑦 ∈ ℋ → ( ( ℋ × { 0 } ) ‘ 𝑦 ) = 0 )
10 9 oveq2d ⊢ ( 𝑦 ∈ ℋ → ( 𝑥 · ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) = ( 𝑥 · 0 ) )
11 mul01 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · 0 ) = 0 )
12 10 11 sylan9eqr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 · ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) = 0 )
13 6 fvconst2 ⊢ ( 𝑧 ∈ ℋ → ( ( ℋ × { 0 } ) ‘ 𝑧 ) = 0 )
14 12 13 oveqan12d ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 · ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) + ( ( ℋ × { 0 } ) ‘ 𝑧 ) ) = ( 0 + 0 ) )
15 00id ⊢ ( 0 + 0 ) = 0
16 14 15 eqtrdi ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 · ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) + ( ( ℋ × { 0 } ) ‘ 𝑧 ) ) = 0 )
17 8 16 eqtr4d ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( ℋ × { 0 } ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) + ( ( ℋ × { 0 } ) ‘ 𝑧 ) ) )
18 17 3impa ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( ℋ × { 0 } ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) + ( ( ℋ × { 0 } ) ‘ 𝑧 ) ) )
19 18 rgen3 ⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( ℋ × { 0 } ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) + ( ( ℋ × { 0 } ) ‘ 𝑧 ) )
20 ellnfn ⊢ ( ( ℋ × { 0 } ) ∈ LinFn ↔ ( ( ℋ × { 0 } ) : ℋ ⟶ ℂ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( ℋ × { 0 } ) ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( ( ℋ × { 0 } ) ‘ 𝑦 ) ) + ( ( ℋ × { 0 } ) ‘ 𝑧 ) ) ) )
21 2 19 20 mpbir2an ⊢ ( ℋ × { 0 } ) ∈ LinFn