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

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 ffvelcdm 
 |-  ( ( S : ~H --> ~H /\ x e. ~H ) -> ( S ` x ) e. ~H )
2 ffvelcdm 
 |-  ( ( 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 ) )