Theorem hoeq

Description: Equality of Hilbert space operators. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hoeq	|- ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A. x e. ~H ( T ` x ) = ( U ` x ) <-> T = U ) )

Proof

Step	Hyp	Ref	Expression
1		ffn	|- ( T : ~H --> ~H -> T Fn ~H )
2		ffn	|- ( U : ~H --> ~H -> U Fn ~H )
3		eqfnfv	|- ( ( T Fn ~H /\ U Fn ~H ) -> ( T = U <-> A. x e. ~H ( T ` x ) = ( U ` x ) ) )
4	3	bicomd	|- ( ( T Fn ~H /\ U Fn ~H ) -> ( A. x e. ~H ( T ` x ) = ( U ` x ) <-> T = U ) )
5	1 2 4	syl2an	|- ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A. x e. ~H ( T ` x ) = ( U ` x ) <-> T = U ) )