Metamath Proof Explorer

Theorem hmopadj

Description: A Hermitian operator is self-adjoint. (Contributed by NM, 24-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopadj ( ๐‘‡ โˆˆ HrmOp โ†’ ( adjโ„Ž โ€˜ ๐‘‡ ) = ๐‘‡ )

Proof

Step Hyp Ref Expression
1 hmopf โŠข ( ๐‘‡ โˆˆ HrmOp โ†’ ๐‘‡ : โ„‹ โŸถ โ„‹ )
2 hmop โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
3 2 eqcomd โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) )
4 3 3expib โŠข ( ๐‘‡ โˆˆ HrmOp โ†’ ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) ) )
5 4 ralrimivv โŠข ( ๐‘‡ โˆˆ HrmOp โ†’ โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) )
6 adjeq โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) ) โ†’ ( adjโ„Ž โ€˜ ๐‘‡ ) = ๐‘‡ )
7 1 1 5 6 syl3anc โŠข ( ๐‘‡ โˆˆ HrmOp โ†’ ( adjโ„Ž โ€˜ ๐‘‡ ) = ๐‘‡ )