# Metamath Proof Explorer

## Theorem hmopre

Description: The inner product of the value and argument of a Hermitian operator is real. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopre ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}\in ℝ$

### Proof

Step Hyp Ref Expression
1 hmop ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in ℋ\wedge {A}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}$
2 1 3anidm23 ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}$
3 2 eqcomd ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}={A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)$
4 hmopf ${⊢}{T}\in \mathrm{HrmOp}\to {T}:ℋ⟶ℋ$
5 4 ffvelrnda ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in ℋ\right)\to {T}\left({A}\right)\in ℋ$
6 hire ${⊢}\left({T}\left({A}\right)\in ℋ\wedge {A}\in ℋ\right)\to \left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}\in ℝ↔{T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}={A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)\right)$
7 5 6 sylancom ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in ℋ\right)\to \left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}\in ℝ↔{T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}={A}{\cdot }_{\mathrm{ih}}{T}\left({A}\right)\right)$
8 3 7 mpbird ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{A}\in ℝ$