Theorem ho02i

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

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

Proof

Step	Hyp	Ref	Expression
1		ho0.1	|- T : ~H --> ~H
2		ralcom	|- ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = 0 <-> A. y e. ~H A. x e. ~H ( x .ih ( T ` y ) ) = 0 )
3	1	ffvelcdmi	|- ( y e. ~H -> ( T ` y ) e. ~H )
4		hial02	|- ( ( T ` y ) e. ~H -> ( A. x e. ~H ( x .ih ( T ` y ) ) = 0 <-> ( T ` y ) = 0h ) )
5		hial0	|- ( ( T ` y ) e. ~H -> ( A. x e. ~H ( ( T ` y ) .ih x ) = 0 <-> ( T ` y ) = 0h ) )
6	4 5	bitr4d	|- ( ( T ` y ) e. ~H -> ( A. x e. ~H ( x .ih ( T ` y ) ) = 0 <-> A. x e. ~H ( ( T ` y ) .ih x ) = 0 ) )
7	3 6	syl	|- ( y e. ~H -> ( A. x e. ~H ( x .ih ( T ` y ) ) = 0 <-> A. x e. ~H ( ( T ` y ) .ih x ) = 0 ) )
8	7	ralbiia	|- ( A. y e. ~H A. x e. ~H ( x .ih ( T ` y ) ) = 0 <-> A. y e. ~H A. x e. ~H ( ( T ` y ) .ih x ) = 0 )
9	1	ho01i	|- ( A. y e. ~H A. x e. ~H ( ( T ` y ) .ih x ) = 0 <-> T = 0hop )
10	2 8 9	3bitri	|- ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = 0 <-> T = 0hop )