# Metamath Proof Explorer

## Theorem hoeq2

Description: A condition implying that two Hilbert space operators are equal. Lemma 3.2(S11) of Beran p. 95. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion hoeq2
`|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( S ` y ) ) = ( x .ih ( T ` y ) ) <-> S = T ) )`

### Proof

Step Hyp Ref Expression
1 ralcom
` |-  ( A. x e. ~H A. y e. ~H ( x .ih ( S ` y ) ) = ( x .ih ( T ` y ) ) <-> A. y e. ~H A. x e. ~H ( x .ih ( S ` y ) ) = ( x .ih ( T ` y ) ) )`
2 1 a1i
` |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( S ` y ) ) = ( x .ih ( T ` y ) ) <-> A. y e. ~H A. x e. ~H ( x .ih ( S ` y ) ) = ( x .ih ( T ` y ) ) ) )`
3 ffvelrn
` |-  ( ( S : ~H --> ~H /\ y e. ~H ) -> ( S ` y ) e. ~H )`
4 ffvelrn
` |-  ( ( T : ~H --> ~H /\ y e. ~H ) -> ( T ` y ) e. ~H )`
5 hial2eq2
` |-  ( ( ( S ` y ) e. ~H /\ ( T ` y ) e. ~H ) -> ( A. x e. ~H ( x .ih ( S ` y ) ) = ( x .ih ( T ` y ) ) <-> ( S ` y ) = ( T ` y ) ) )`
6 hial2eq
` |-  ( ( ( S ` y ) e. ~H /\ ( T ` y ) e. ~H ) -> ( A. x e. ~H ( ( S ` y ) .ih x ) = ( ( T ` y ) .ih x ) <-> ( S ` y ) = ( T ` y ) ) )`
7 5 6 bitr4d
` |-  ( ( ( S ` y ) e. ~H /\ ( T ` y ) e. ~H ) -> ( A. x e. ~H ( x .ih ( S ` y ) ) = ( x .ih ( T ` y ) ) <-> A. x e. ~H ( ( S ` y ) .ih x ) = ( ( T ` y ) .ih x ) ) )`
8 3 4 7 syl2an
` |-  ( ( ( S : ~H --> ~H /\ y e. ~H ) /\ ( T : ~H --> ~H /\ y e. ~H ) ) -> ( A. x e. ~H ( x .ih ( S ` y ) ) = ( x .ih ( T ` y ) ) <-> A. x e. ~H ( ( S ` y ) .ih x ) = ( ( T ` y ) .ih x ) ) )`
9 8 anandirs
` |-  ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ y e. ~H ) -> ( A. x e. ~H ( x .ih ( S ` y ) ) = ( x .ih ( T ` y ) ) <-> A. x e. ~H ( ( S ` y ) .ih x ) = ( ( T ` y ) .ih x ) ) )`
10 9 ralbidva
` |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( A. y e. ~H A. x e. ~H ( x .ih ( S ` y ) ) = ( x .ih ( T ` y ) ) <-> A. y e. ~H A. x e. ~H ( ( S ` y ) .ih x ) = ( ( T ` y ) .ih x ) ) )`
11 hoeq1
` |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( A. y e. ~H A. x e. ~H ( ( S ` y ) .ih x ) = ( ( T ` y ) .ih x ) <-> S = T ) )`
12 2 10 11 3bitrd
` |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( x .ih ( S ` y ) ) = ( x .ih ( T ` y ) ) <-> S = T ) )`