# 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 ffvelrni
` |-  ( 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 )`