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