Metamath Proof Explorer

Theorem hmopm

Description: The scalar product of a Hermitian operator with a real is Hermitian. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopm ⊢ A ∈ ℝ ∧ T ∈ HrmOp → A · op T ∈ HrmOp

Proof

Step Hyp Ref Expression
1 recn ⊢ A ∈ ℝ → A ∈ ℂ
2 hmopf ⊢ T ∈ HrmOp → T : ℋ ⟶ ℋ
3 homulcl ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op T : ℋ ⟶ ℋ
4 1 2 3 syl2an ⊢ A ∈ ℝ ∧ T ∈ HrmOp → A · op T : ℋ ⟶ ℋ
5 cjre ⊢ A ∈ ℝ → A ‾ = A
6 hmop ⊢ T ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
7 6 3expb ⊢ T ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
8 5 7 oveqan12d ⊢ A ∈ ℝ ∧ T ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → A ‾ ⁢ x ⋅ ih T ⁡ y = A ⁢ T ⁡ x ⋅ ih y
9 8 anassrs ⊢ A ∈ ℝ ∧ T ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → A ‾ ⁢ x ⋅ ih T ⁡ y = A ⁢ T ⁡ x ⋅ ih y
10 1 2 anim12i ⊢ A ∈ ℝ ∧ T ∈ HrmOp → A ∈ ℂ ∧ T : ℋ ⟶ ℋ
11 homval ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ y ∈ ℋ → A · op T ⁡ y = A ⋅ ℎ T ⁡ y
12 11 3expa ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ y ∈ ℋ → A · op T ⁡ y = A ⋅ ℎ T ⁡ y
13 12 adantrl ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → A · op T ⁡ y = A ⋅ ℎ T ⁡ y
14 13 oveq2d ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih A · op T ⁡ y = x ⋅ ih A ⋅ ℎ T ⁡ y
15 simpll ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → A ∈ ℂ
16 simprl ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → x ∈ ℋ
17 ffvelcdm ⊢ T : ℋ ⟶ ℋ ∧ y ∈ ℋ → T ⁡ y ∈ ℋ
18 17 ad2ant2l ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ y ∈ ℋ
19 his5 ⊢ A ∈ ℂ ∧ x ∈ ℋ ∧ T ⁡ y ∈ ℋ → x ⋅ ih A ⋅ ℎ T ⁡ y = A ‾ ⁢ x ⋅ ih T ⁡ y
20 15 16 18 19 syl3anc ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih A ⋅ ℎ T ⁡ y = A ‾ ⁢ x ⋅ ih T ⁡ y
21 14 20 eqtrd ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih A · op T ⁡ y = A ‾ ⁢ x ⋅ ih T ⁡ y
22 10 21 sylan ⊢ A ∈ ℝ ∧ T ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih A · op T ⁡ y = A ‾ ⁢ x ⋅ ih T ⁡ y
23 homval ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A · op T ⁡ x = A ⋅ ℎ T ⁡ x
24 23 3expa ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A · op T ⁡ x = A ⋅ ℎ T ⁡ x
25 24 adantrr ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → A · op T ⁡ x = A ⋅ ℎ T ⁡ x
26 25 oveq1d ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → A · op T ⁡ x ⋅ ih y = A ⋅ ℎ T ⁡ x ⋅ ih y
27 ffvelcdm ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → T ⁡ x ∈ ℋ
28 27 ad2ant2lr ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ∈ ℋ
29 simprr ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → y ∈ ℋ
30 ax-his3 ⊢ A ∈ ℂ ∧ T ⁡ x ∈ ℋ ∧ y ∈ ℋ → A ⋅ ℎ T ⁡ x ⋅ ih y = A ⁢ T ⁡ x ⋅ ih y
31 15 28 29 30 syl3anc ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → A ⋅ ℎ T ⁡ x ⋅ ih y = A ⁢ T ⁡ x ⋅ ih y
32 26 31 eqtrd ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → A · op T ⁡ x ⋅ ih y = A ⁢ T ⁡ x ⋅ ih y
33 10 32 sylan ⊢ A ∈ ℝ ∧ T ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → A · op T ⁡ x ⋅ ih y = A ⁢ T ⁡ x ⋅ ih y
34 9 22 33 3eqtr4d ⊢ A ∈ ℝ ∧ T ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih A · op T ⁡ y = A · op T ⁡ x ⋅ ih y
35 34 ralrimivva ⊢ A ∈ ℝ ∧ T ∈ HrmOp → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih A · op T ⁡ y = A · op T ⁡ x ⋅ ih y
36 elhmop ⊢ A · op T ∈ HrmOp ↔ A · op T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih A · op T ⁡ y = A · op T ⁡ x ⋅ ih y
37 4 35 36 sylanbrc ⊢ A ∈ ℝ ∧ T ∈ HrmOp → A · op T ∈ HrmOp