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·opT∈HrmOp

Proof

Step Hyp Ref Expression
1 recn ⊢A∈ℝ→A∈ℂ
2 hmopf ⊢T∈HrmOp→T:ℋ⟶ℋ
3 homulcl ⊢A∈ℂ∧T:ℋ⟶ℋ→A·opT:ℋ⟶ℋ
4 1 2 3 syl2an ⊢A∈ℝ∧T∈HrmOp→A·opT:ℋ⟶ℋ
5 cjre ⊢A∈ℝ→A‾=A
6 hmop ⊢T∈HrmOp∧x∈ℋ∧y∈ℋ→x⋅ihT⁡y=T⁡x⋅ihy
7 6 3expb ⊢T∈HrmOp∧x∈ℋ∧y∈ℋ→x⋅ihT⁡y=T⁡x⋅ihy
8 5 7 oveqan12d ⊢A∈ℝ∧T∈HrmOp∧x∈ℋ∧y∈ℋ→A‾⁢x⋅ihT⁡y=A⁢T⁡x⋅ihy
9 8 anassrs ⊢A∈ℝ∧T∈HrmOp∧x∈ℋ∧y∈ℋ→A‾⁢x⋅ihT⁡y=A⁢T⁡x⋅ihy
10 1 2 anim12i ⊢A∈ℝ∧T∈HrmOp→A∈ℂ∧T:ℋ⟶ℋ
11 homval ⊢A∈ℂ∧T:ℋ⟶ℋ∧y∈ℋ→A·opT⁡y=A⋅ℎT⁡y
12 11 3expa ⊢A∈ℂ∧T:ℋ⟶ℋ∧y∈ℋ→A·opT⁡y=A⋅ℎT⁡y
13 12 adantrl ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→A·opT⁡y=A⋅ℎT⁡y
14 13 oveq2d ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→x⋅ihA·opT⁡y=x⋅ihA⋅ℎ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⋅ihA⋅ℎT⁡y=A‾⁢x⋅ihT⁡y
20 15 16 18 19 syl3anc ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→x⋅ihA⋅ℎT⁡y=A‾⁢x⋅ihT⁡y
21 14 20 eqtrd ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→x⋅ihA·opT⁡y=A‾⁢x⋅ihT⁡y
22 10 21 sylan ⊢A∈ℝ∧T∈HrmOp∧x∈ℋ∧y∈ℋ→x⋅ihA·opT⁡y=A‾⁢x⋅ihT⁡y
23 homval ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A·opT⁡x=A⋅ℎT⁡x
24 23 3expa ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A·opT⁡x=A⋅ℎT⁡x
25 24 adantrr ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→A·opT⁡x=A⋅ℎT⁡x
26 25 oveq1d ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→A·opT⁡x⋅ihy=A⋅ℎT⁡x⋅ihy
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⋅ihy=A⁢T⁡x⋅ihy
31 15 28 29 30 syl3anc ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→A⋅ℎT⁡x⋅ihy=A⁢T⁡x⋅ihy
32 26 31 eqtrd ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ∧y∈ℋ→A·opT⁡x⋅ihy=A⁢T⁡x⋅ihy
33 10 32 sylan ⊢A∈ℝ∧T∈HrmOp∧x∈ℋ∧y∈ℋ→A·opT⁡x⋅ihy=A⁢T⁡x⋅ihy
34 9 22 33 3eqtr4d ⊢A∈ℝ∧T∈HrmOp∧x∈ℋ∧y∈ℋ→x⋅ihA·opT⁡y=A·opT⁡x⋅ihy
35 34 ralrimivva ⊢A∈ℝ∧T∈HrmOp→∀x∈ℋ∀y∈ℋx⋅ihA·opT⁡y=A·opT⁡x⋅ihy
36 elhmop ⊢A·opT∈HrmOp↔A·opT:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihA·opT⁡y=A·opT⁡x⋅ihy
37 4 35 36 sylanbrc ⊢A∈ℝ∧T∈HrmOp→A·opT∈HrmOp