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 ) )