Theorem lnfn0i

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

	Ref	Expression
Hypothesis	lnfnl.1	|- T e. LinFn
Assertion	lnfn0i	|- ( T ` 0h ) = 0

Proof

Step	Hyp	Ref	Expression
1		lnfnl.1	|- T e. LinFn
2		ax-hv0cl	|- 0h e. ~H
3	1	lnfnfi	|- T : ~H --> CC
4	3	ffvelcdmi	|- ( 0h e. ~H -> ( T ` 0h ) e. CC )
5	2 4	ax-mp	|- ( T ` 0h ) e. CC
6	5 5	pncan3oi	|- ( ( ( T ` 0h ) + ( T ` 0h ) ) - ( T ` 0h ) ) = ( T ` 0h )
7		ax-1cn	|- 1 e. CC
8	1	lnfnli	|- ( ( 1 e. CC /\ 0h e. ~H /\ 0h e. ~H ) -> ( T ` ( ( 1 .h 0h ) +h 0h ) ) = ( ( 1 x. ( T ` 0h ) ) + ( T ` 0h ) ) )
9	7 2 2 8	mp3an	|- ( T ` ( ( 1 .h 0h ) +h 0h ) ) = ( ( 1 x. ( T ` 0h ) ) + ( T ` 0h ) )
10	7 2	hvmulcli	|- ( 1 .h 0h ) e. ~H
11		ax-hvaddid	|- ( ( 1 .h 0h ) e. ~H -> ( ( 1 .h 0h ) +h 0h ) = ( 1 .h 0h ) )
12	10 11	ax-mp	|- ( ( 1 .h 0h ) +h 0h ) = ( 1 .h 0h )
13		ax-hvmulid	|- ( 0h e. ~H -> ( 1 .h 0h ) = 0h )
14	2 13	ax-mp	|- ( 1 .h 0h ) = 0h
15	12 14	eqtri	|- ( ( 1 .h 0h ) +h 0h ) = 0h
16	15	fveq2i	|- ( T ` ( ( 1 .h 0h ) +h 0h ) ) = ( T ` 0h )
17	9 16	eqtr3i	|- ( ( 1 x. ( T ` 0h ) ) + ( T ` 0h ) ) = ( T ` 0h )
18	5	mullidi	|- ( 1 x. ( T ` 0h ) ) = ( T ` 0h )
19	18	oveq1i	|- ( ( 1 x. ( T ` 0h ) ) + ( T ` 0h ) ) = ( ( T ` 0h ) + ( T ` 0h ) )
20	17 19	eqtr3i	|- ( T ` 0h ) = ( ( T ` 0h ) + ( T ` 0h ) )
21	20	oveq1i	|- ( ( T ` 0h ) - ( T ` 0h ) ) = ( ( ( T ` 0h ) + ( T ` 0h ) ) - ( T ` 0h ) )
22	5	subidi	|- ( ( T ` 0h ) - ( T ` 0h ) ) = 0
23	21 22	eqtr3i	|- ( ( ( T ` 0h ) + ( T ` 0h ) ) - ( T ` 0h ) ) = 0
24	6 23	eqtr3i	|- ( T ` 0h ) = 0