Theorem ho01i

Description: A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S8) of Beran p. 95. (Contributed by NM, 28-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ho0.1	|- T : ~H --> ~H
Assertion	ho01i	|- ( A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = 0 <-> T = 0hop )

Proof

Step	Hyp	Ref	Expression
1		ho0.1	|- T : ~H --> ~H
2		ffn	|- ( T : ~H --> ~H -> T Fn ~H )
3	1 2	ax-mp	|- T Fn ~H
4		ax-hv0cl	|- 0h e. ~H
5	4	elexi	|- 0h e. _V
6	5	fconst	|- ( ~H X. { 0h } ) : ~H --> { 0h }
7		ffn	|- ( ( ~H X. { 0h } ) : ~H --> { 0h } -> ( ~H X. { 0h } ) Fn ~H )
8	6 7	ax-mp	|- ( ~H X. { 0h } ) Fn ~H
9		eqfnfv	|- ( ( T Fn ~H /\ ( ~H X. { 0h } ) Fn ~H ) -> ( T = ( ~H X. { 0h } ) <-> A. x e. ~H ( T ` x ) = ( ( ~H X. { 0h } ) ` x ) ) )
10	3 8 9	mp2an	|- ( T = ( ~H X. { 0h } ) <-> A. x e. ~H ( T ` x ) = ( ( ~H X. { 0h } ) ` x ) )
11		df0op2	|- 0hop = ( ~H X. 0H )
12		df-ch0	|- 0H = { 0h }
13	12	xpeq2i	|- ( ~H X. 0H ) = ( ~H X. { 0h } )
14	11 13	eqtri	|- 0hop = ( ~H X. { 0h } )
15	14	eqeq2i	|- ( T = 0hop <-> T = ( ~H X. { 0h } ) )
16	1	ffvelcdmi	|- ( x e. ~H -> ( T ` x ) e. ~H )
17		hial0	|- ( ( T ` x ) e. ~H -> ( A. y e. ~H ( ( T ` x ) .ih y ) = 0 <-> ( T ` x ) = 0h ) )
18	16 17	syl	|- ( x e. ~H -> ( A. y e. ~H ( ( T ` x ) .ih y ) = 0 <-> ( T ` x ) = 0h ) )
19	5	fvconst2	|- ( x e. ~H -> ( ( ~H X. { 0h } ) ` x ) = 0h )
20	19	eqeq2d	|- ( x e. ~H -> ( ( T ` x ) = ( ( ~H X. { 0h } ) ` x ) <-> ( T ` x ) = 0h ) )
21	18 20	bitr4d	|- ( x e. ~H -> ( A. y e. ~H ( ( T ` x ) .ih y ) = 0 <-> ( T ` x ) = ( ( ~H X. { 0h } ) ` x ) ) )
22	21	ralbiia	|- ( A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = 0 <-> A. x e. ~H ( T ` x ) = ( ( ~H X. { 0h } ) ` x ) )
23	10 15 22	3bitr4ri	|- ( A. x e. ~H A. y e. ~H ( ( T ` x ) .ih y ) = 0 <-> T = 0hop )