# 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 ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\right)\to {A}{·}_{\mathrm{op}}{T}\in \mathrm{HrmOp}$

### Proof

Step Hyp Ref Expression
1 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
2 hmopf ${⊢}{T}\in \mathrm{HrmOp}\to {T}:ℋ⟶ℋ$
3 homulcl ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
4 1 2 3 syl2an ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\right)\to \left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
5 cjre ${⊢}{A}\in ℝ\to \stackrel{‾}{{A}}={A}$
6 hmop ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
7 6 3expb ${⊢}\left({T}\in \mathrm{HrmOp}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
8 5 7 oveqan12d ${⊢}\left({A}\in ℝ\wedge \left({T}\in \mathrm{HrmOp}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\right)\to \stackrel{‾}{{A}}\left({x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)={A}\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
9 8 anassrs ${⊢}\left(\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \stackrel{‾}{{A}}\left({x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)={A}\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
10 1 2 anim12i ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\right)\to \left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)$
11 homval ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)={A}{\cdot }_{ℎ}{T}\left({y}\right)$
12 11 3expa ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge {y}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)={A}{\cdot }_{ℎ}{T}\left({y}\right)$
13 12 adantrl ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)={A}{\cdot }_{ℎ}{T}\left({y}\right)$
14 13 oveq2d ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{T}\left({y}\right)\right)$
15 simpll ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {A}\in ℂ$
16 simprl ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}\in ℋ$
17 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\to {T}\left({y}\right)\in ℋ$
18 17 ad2ant2l ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {T}\left({y}\right)\in ℋ$
19 his5 ${⊢}\left({A}\in ℂ\wedge {x}\in ℋ\wedge {T}\left({y}\right)\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{T}\left({y}\right)\right)=\stackrel{‾}{{A}}\left({x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)$
20 15 16 18 19 syl3anc ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{T}\left({y}\right)\right)=\stackrel{‾}{{A}}\left({x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)$
21 14 20 eqtrd ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)=\stackrel{‾}{{A}}\left({x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)$
22 10 21 sylan ${⊢}\left(\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)=\stackrel{‾}{{A}}\left({x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)$
23 homval ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)={A}{\cdot }_{ℎ}{T}\left({x}\right)$
24 23 3expa ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)={A}{\cdot }_{ℎ}{T}\left({x}\right)$
25 24 adantrr ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)={A}{\cdot }_{ℎ}{T}\left({x}\right)$
26 25 oveq1d ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}=\left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}$
27 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {T}\left({x}\right)\in ℋ$
28 27 ad2ant2lr ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {T}\left({x}\right)\in ℋ$
29 simprr ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {y}\in ℋ$
30 ax-his3 ${⊢}\left({A}\in ℂ\wedge {T}\left({x}\right)\in ℋ\wedge {y}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}={A}\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
31 15 28 29 30 syl3anc ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}={A}\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
32 26 31 eqtrd ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={A}\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
33 10 32 sylan ${⊢}\left(\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={A}\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
34 9 22 33 3eqtr4d ${⊢}\left(\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)=\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
35 34 ralrimivva ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)=\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
36 elhmop ${⊢}{A}{·}_{\mathrm{op}}{T}\in \mathrm{HrmOp}↔\left(\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}\left({A}{·}_{\mathrm{op}}{T}\right)\left({y}\right)=\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
37 4 35 36 sylanbrc ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\right)\to {A}{·}_{\mathrm{op}}{T}\in \mathrm{HrmOp}$