Theorem lnfn0

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

	Ref	Expression
Assertion	lnfn0	⊢ ( 𝑇 ∈ LinFn → ( 𝑇 ‘ 0ℎ ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		fveq1	⊢ ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( 𝑇 ‘ 0ℎ ) = ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 0ℎ ) )
2	1	eqeq1d	⊢ ( 𝑇 = if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) → ( ( 𝑇 ‘ 0ℎ ) = 0 ↔ ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 0ℎ ) = 0 ) )
3		0lnfn	⊢ ( ℋ × { 0 } ) ∈ LinFn
4	3	elimel	⊢ if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ∈ LinFn
5	4	lnfn0i	⊢ ( if ( 𝑇 ∈ LinFn , 𝑇 , ( ℋ × { 0 } ) ) ‘ 0ℎ ) = 0
6	2 5	dedth	⊢ ( 𝑇 ∈ LinFn → ( 𝑇 ‘ 0ℎ ) = 0 )