Theorem elhmop

Description: Property defining a Hermitian Hilbert space operator. (Contributed by NM, 18-Jan-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		fveq1	|- ( t = T -> ( t ` y ) = ( T ` y ) )
2	1	oveq2d	|- ( t = T -> ( x .ih ( t ` y ) ) = ( x .ih ( T ` y ) ) )
3		fveq1	|- ( t = T -> ( t ` x ) = ( T ` x ) )
4	3	oveq1d	|- ( t = T -> ( ( t ` x ) .ih y ) = ( ( T ` x ) .ih y ) )
5	2 4	eqeq12d	|- ( t = T -> ( ( x .ih ( t ` y ) ) = ( ( t ` x ) .ih y ) <-> ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) ) )
6	5	2ralbidv	|- ( t = T -> ( A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( t ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) ) )
7		df-hmop	|- HrmOp = { t e. ( ~H ^m ~H ) | A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( t ` x ) .ih y ) }
8	6 7	elrab2	|- ( T e. HrmOp <-> ( T e. ( ~H ^m ~H ) /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) ) )
9		ax-hilex	|- ~H e. _V
10	9 9	elmap	|- ( T e. ( ~H ^m ~H ) <-> T : ~H --> ~H )
11	10	anbi1i	|- ( ( T e. ( ~H ^m ~H ) /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) ) <-> ( T : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) ) )
12	8 11	bitri	|- ( T e. HrmOp <-> ( T : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) ) )