# 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$