This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )