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

Metamath Proof Explorer

Theorem adjmo

Description: Every Hilbert space operator has at most one adjoint. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	adjmo	\|- E* u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) )

Proof

Step	Hyp	Ref	Expression
1		r19.26-2	\|- ( A. x e. ~H A. y e. ~H ( ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) /\ ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) <-> ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) )
2		eqtr2	\|- ( ( ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) /\ ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) -> ( ( u ` x ) .ih y ) = ( ( v ` x ) .ih y ) )
3	2	2ralimi	\|- ( A. x e. ~H A. y e. ~H ( ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) /\ ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) -> A. x e. ~H A. y e. ~H ( ( u ` x ) .ih y ) = ( ( v ` x ) .ih y ) )
4	1 3	sylbir	\|- ( ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) -> A. x e. ~H A. y e. ~H ( ( u ` x ) .ih y ) = ( ( v ` x ) .ih y ) )
5		hoeq1	\|- ( ( u : ~H --> ~H /\ v : ~H --> ~H ) -> ( A. x e. ~H A. y e. ~H ( ( u ` x ) .ih y ) = ( ( v ` x ) .ih y ) <-> u = v ) )
6	5	biimpa	\|- ( ( ( u : ~H --> ~H /\ v : ~H --> ~H ) /\ A. x e. ~H A. y e. ~H ( ( u ` x ) .ih y ) = ( ( v ` x ) .ih y ) ) -> u = v )
7	4 6	sylan2	\|- ( ( ( u : ~H --> ~H /\ v : ~H --> ~H ) /\ ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) ) -> u = v )
8	7	an4s	\|- ( ( ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) /\ ( v : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) ) -> u = v )
9	8	gen2	\|- A. u A. v ( ( ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) /\ ( v : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) ) -> u = v )
10		feq1	\|- ( u = v -> ( u : ~H --> ~H <-> v : ~H --> ~H ) )
11		fveq1	\|- ( u = v -> ( u ` x ) = ( v ` x ) )
12	11	oveq1d	\|- ( u = v -> ( ( u ` x ) .ih y ) = ( ( v ` x ) .ih y ) )
13	12	eqeq2d	\|- ( u = v -> ( ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) <-> ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) )
14	13	2ralbidv	\|- ( u = v -> ( A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) )
15	10 14	anbi12d	\|- ( u = v -> ( ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( v : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) ) )
16	15	mo4	\|- ( E* u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) <-> A. u A. v ( ( ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) /\ ( v : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( v ` x ) .ih y ) ) ) -> u = v ) )
17	9 16	mpbir	\|- E* u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) )