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