Metamath Proof Explorer

Theorem unopadj2

Description: The adjoint of a unitary operator is its inverse (converse). Equation 2 of AkhiezerGlazman p. 72. (Contributed by NM, 23-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion unopadj2 ( ๐‘‡ โˆˆ UniOp โ†’ ( adjโ„Ž โ€˜ ๐‘‡ ) = โ—ก ๐‘‡ )

Proof

Step Hyp Ref Expression
1 unoplin โŠข ( ๐‘‡ โˆˆ UniOp โ†’ ๐‘‡ โˆˆ LinOp )
2 lnopf โŠข ( ๐‘‡ โˆˆ LinOp โ†’ ๐‘‡ : โ„‹ โŸถ โ„‹ )
3 1 2 syl โŠข ( ๐‘‡ โˆˆ UniOp โ†’ ๐‘‡ : โ„‹ โŸถ โ„‹ )
4 cnvunop โŠข ( ๐‘‡ โˆˆ UniOp โ†’ โ—ก ๐‘‡ โˆˆ UniOp )
5 unoplin โŠข ( โ—ก ๐‘‡ โˆˆ UniOp โ†’ โ—ก ๐‘‡ โˆˆ LinOp )
6 lnopf โŠข ( โ—ก ๐‘‡ โˆˆ LinOp โ†’ โ—ก ๐‘‡ : โ„‹ โŸถ โ„‹ )
7 4 5 6 3syl โŠข ( ๐‘‡ โˆˆ UniOp โ†’ โ—ก ๐‘‡ : โ„‹ โŸถ โ„‹ )
8 unopadj โŠข ( ( ๐‘‡ โˆˆ UniOp โˆง ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ๐‘ฅ ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ฆ ) ) )
9 8 3expib โŠข ( ๐‘‡ โˆˆ UniOp โ†’ ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ๐‘ฅ ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ฆ ) ) ) )
10 9 ralrimivv โŠข ( ๐‘‡ โˆˆ UniOp โ†’ โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ๐‘ฅ ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ฆ ) ) )
11 adjeq โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง โ—ก ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ๐‘ฅ ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ฆ ) ) ) โ†’ ( adjโ„Ž โ€˜ ๐‘‡ ) = โ—ก ๐‘‡ )
12 3 7 10 11 syl3anc โŠข ( ๐‘‡ โˆˆ UniOp โ†’ ( adjโ„Ž โ€˜ ๐‘‡ ) = โ—ก ๐‘‡ )