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 ⊢ x ∈ ℂ ∧ y ∈ ℋ → x ⋅ ℎ y ∈ ℋ
4 hvaddcl ⊢ x ⋅ ℎ y ∈ ℋ ∧ z ∈ ℋ → x ⋅ ℎ y + ℎ z ∈ ℋ
5 3 4 sylan ⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → x ⋅ ℎ y + ℎ z ∈ ℋ
6 c0ex ⊢ 0 ∈ V
7 6 fvconst2 ⊢ x ⋅ ℎ y + ℎ z ∈ ℋ → ℋ × 0 ⁡ x ⋅ ℎ y + ℎ z = 0
8 5 7 syl ⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → ℋ × 0 ⁡ x ⋅ ℎ y + ℎ z = 0
9 6 fvconst2 ⊢ y ∈ ℋ → ℋ × 0 ⁡ y = 0
10 9 oveq2d ⊢ y ∈ ℋ → x ⁢ ℋ × 0 ⁡ y = x ⋅ 0
11 mul01 ⊢ x ∈ ℂ → x ⋅ 0 = 0
12 10 11 sylan9eqr ⊢ x ∈ ℂ ∧ y ∈ ℋ → x ⁢ ℋ × 0 ⁡ y = 0
13 6 fvconst2 ⊢ z ∈ ℋ → ℋ × 0 ⁡ z = 0
14 12 13 oveqan12d ⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → x ⁢ ℋ × 0 ⁡ y + ℋ × 0 ⁡ z = 0 + 0
15 00id ⊢ 0 + 0 = 0
16 14 15 eqtrdi ⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → x ⁢ ℋ × 0 ⁡ y + ℋ × 0 ⁡ z = 0
17 8 16 eqtr4d ⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → ℋ × 0 ⁡ x ⋅ ℎ y + ℎ z = x ⁢ ℋ × 0 ⁡ y + ℋ × 0 ⁡ z
18 17 3impa ⊢ x ∈ ℂ ∧ y ∈ ℋ ∧ z ∈ ℋ → ℋ × 0 ⁡ x ⋅ ℎ y + ℎ z = x ⁢ ℋ × 0 ⁡ y + ℋ × 0 ⁡ z
19 18 rgen3 ⊢ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ ℋ × 0 ⁡ x ⋅ ℎ y + ℎ z = x ⁢ ℋ × 0 ⁡ y + ℋ × 0 ⁡ z
20 ellnfn ⊢ ℋ × 0 ∈ LinFn ↔ ℋ × 0 : ℋ ⟶ ℂ ∧ ∀ x ∈ ℂ ∀ y ∈ ℋ ∀ z ∈ ℋ ℋ × 0 ⁡ x ⋅ ℎ y + ℎ z = x ⁢ ℋ × 0 ⁡ y + ℋ × 0 ⁡ z
21 2 19 20 mpbir2an ⊢ ℋ × 0 ∈ LinFn