# Metamath Proof Explorer

## Theorem hoeq1

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

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

### Proof

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