This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ) → ( 𝐴 ·op 𝑇 ) ∈ HrmOp )

Proof

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