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		ffvelrn	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
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		ffvelrn	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
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 )