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	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		hmop	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 ·ih ( 𝑇 ‘ 𝐴 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) )
2	1	3anidm23	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ℋ ) → ( 𝐴 ·ih ( 𝑇 ‘ 𝐴 ) ) = ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) )
3	2	eqcomd	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) = ( 𝐴 ·ih ( 𝑇 ‘ 𝐴 ) ) )
4		hmopf	⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )
5	4	ffvelcdmda	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ℋ ) → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
6		hire	⊢ ( ( ( 𝑇 ‘ 𝐴 ) ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) ∈ ℝ ↔ ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) = ( 𝐴 ·ih ( 𝑇 ‘ 𝐴 ) ) ) )
7	5 6	sylancom	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ℋ ) → ( ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) ∈ ℝ ↔ ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) = ( 𝐴 ·ih ( 𝑇 ‘ 𝐴 ) ) ) )
8	3 7	mpbird	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝐴 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·ih 𝐴 ) ∈ ℝ )