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 โˆƒ* ๐‘ข ( ๐‘ข : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )

Proof

Step Hyp Ref Expression
1 r19.26-2 โŠข ( โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) โˆง ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) โ†” ( โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) )
2 eqtr2 โŠข ( ( ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) โˆง ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) โ†’ ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
3 2 2ralimi โŠข ( โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) โˆง ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) โ†’ โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
4 1 3 sylbir โŠข ( ( โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) โ†’ โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
5 hoeq1 โŠข ( ( ๐‘ข : โ„‹ โŸถ โ„‹ โˆง ๐‘ฃ : โ„‹ โŸถ โ„‹ ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) โ†” ๐‘ข = ๐‘ฃ ) )
6 5 biimpa โŠข ( ( ( ๐‘ข : โ„‹ โŸถ โ„‹ โˆง ๐‘ฃ : โ„‹ โŸถ โ„‹ ) โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) โ†’ ๐‘ข = ๐‘ฃ )
7 4 6 sylan2 โŠข ( ( ( ๐‘ข : โ„‹ โŸถ โ„‹ โˆง ๐‘ฃ : โ„‹ โŸถ โ„‹ ) โˆง ( โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) ) โ†’ ๐‘ข = ๐‘ฃ )
8 7 an4s โŠข ( ( ( ๐‘ข : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) โˆง ( ๐‘ฃ : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) ) โ†’ ๐‘ข = ๐‘ฃ )
9 8 gen2 โŠข โˆ€ ๐‘ข โˆ€ ๐‘ฃ ( ( ( ๐‘ข : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) โˆง ( ๐‘ฃ : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) ) โ†’ ๐‘ข = ๐‘ฃ )
10 feq1 โŠข ( ๐‘ข = ๐‘ฃ โ†’ ( ๐‘ข : โ„‹ โŸถ โ„‹ โ†” ๐‘ฃ : โ„‹ โŸถ โ„‹ ) )
11 fveq1 โŠข ( ๐‘ข = ๐‘ฃ โ†’ ( ๐‘ข โ€˜ ๐‘ฅ ) = ( ๐‘ฃ โ€˜ ๐‘ฅ ) )
12 11 oveq1d โŠข ( ๐‘ข = ๐‘ฃ โ†’ ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
13 12 eqeq2d โŠข ( ๐‘ข = ๐‘ฃ โ†’ ( ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) โ†” ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) )
14 13 2ralbidv โŠข ( ๐‘ข = ๐‘ฃ โ†’ ( โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) โ†” โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) )
15 10 14 anbi12d โŠข ( ๐‘ข = ๐‘ฃ โ†’ ( ( ๐‘ข : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) โ†” ( ๐‘ฃ : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) ) )
16 15 mo4 โŠข ( โˆƒ* ๐‘ข ( ๐‘ข : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) โ†” โˆ€ ๐‘ข โˆ€ ๐‘ฃ ( ( ( ๐‘ข : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) โˆง ( ๐‘ฃ : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ฃ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) ) โ†’ ๐‘ข = ๐‘ฃ ) )
17 9 16 mpbir โŠข โˆƒ* ๐‘ข ( ๐‘ข : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ข โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )