# Metamath Proof Explorer

## Theorem hmops

Description: The sum of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion hmops ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {U}\in \mathrm{HrmOp}\right)\to {T}{+}_{\mathrm{op}}{U}\in \mathrm{HrmOp}$

### Proof

Step Hyp Ref Expression
1 hmopf ${⊢}{T}\in \mathrm{HrmOp}\to {T}:ℋ⟶ℋ$
2 hmopf ${⊢}{U}\in \mathrm{HrmOp}\to {U}:ℋ⟶ℋ$
3 hoaddcl ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({T}{+}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
4 1 2 3 syl2an ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {U}\in \mathrm{HrmOp}\right)\to \left({T}{+}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
5 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}$
6 5 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}$
7 hmop ${⊢}\left({U}\in \mathrm{HrmOp}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}{U}\left({y}\right)={U}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
8 7 3expb ${⊢}\left({U}\in \mathrm{HrmOp}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}{U}\left({y}\right)={U}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
9 6 8 oveqan12d ${⊢}\left(\left({T}\in \mathrm{HrmOp}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\wedge \left({U}\in \mathrm{HrmOp}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\right)\to \left({x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)+\left({x}{\cdot }_{\mathrm{ih}}{U}\left({y}\right)\right)=\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({U}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
10 9 anandirs ${⊢}\left(\left({T}\in \mathrm{HrmOp}\wedge {U}\in \mathrm{HrmOp}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)+\left({x}{\cdot }_{\mathrm{ih}}{U}\left({y}\right)\right)=\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({U}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
11 1 2 anim12i ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {U}\in \mathrm{HrmOp}\right)\to \left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)$
12 hosval ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\to \left({T}{+}_{\mathrm{op}}{U}\right)\left({y}\right)={T}\left({y}\right){+}_{ℎ}{U}\left({y}\right)$
13 12 oveq2d ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}\left({T}{+}_{\mathrm{op}}{U}\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}\left({T}\left({y}\right){+}_{ℎ}{U}\left({y}\right)\right)$
14 13 3expa ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {y}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}\left({T}{+}_{\mathrm{op}}{U}\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}\left({T}\left({y}\right){+}_{ℎ}{U}\left({y}\right)\right)$
15 14 adantrl ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}\left({T}{+}_{\mathrm{op}}{U}\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}\left({T}\left({y}\right){+}_{ℎ}{U}\left({y}\right)\right)$
16 simprl ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\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 ad2ant2rl ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {T}\left({y}\right)\in ℋ$
19 ffvelrn ${⊢}\left({U}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\to {U}\left({y}\right)\in ℋ$
20 19 ad2ant2l ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {U}\left({y}\right)\in ℋ$
21 his7 ${⊢}\left({x}\in ℋ\wedge {T}\left({y}\right)\in ℋ\wedge {U}\left({y}\right)\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}\left({T}\left({y}\right){+}_{ℎ}{U}\left({y}\right)\right)=\left({x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)+\left({x}{\cdot }_{\mathrm{ih}}{U}\left({y}\right)\right)$
22 16 18 20 21 syl3anc ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}\left({T}\left({y}\right){+}_{ℎ}{U}\left({y}\right)\right)=\left({x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)+\left({x}{\cdot }_{\mathrm{ih}}{U}\left({y}\right)\right)$
23 15 22 eqtrd ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}\left({T}{+}_{\mathrm{op}}{U}\right)\left({y}\right)=\left({x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)+\left({x}{\cdot }_{\mathrm{ih}}{U}\left({y}\right)\right)$
24 11 23 sylan ${⊢}\left(\left({T}\in \mathrm{HrmOp}\wedge {U}\in \mathrm{HrmOp}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}\left({T}{+}_{\mathrm{op}}{U}\right)\left({y}\right)=\left({x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)+\left({x}{\cdot }_{\mathrm{ih}}{U}\left({y}\right)\right)$
25 hosval ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right)={T}\left({x}\right){+}_{ℎ}{U}\left({x}\right)$
26 25 oveq1d ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}=\left({T}\left({x}\right){+}_{ℎ}{U}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}$
27 26 3expa ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}=\left({T}\left({x}\right){+}_{ℎ}{U}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}$
28 27 adantrr ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}=\left({T}\left({x}\right){+}_{ℎ}{U}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}$
29 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {T}\left({x}\right)\in ℋ$
30 29 ad2ant2r ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {T}\left({x}\right)\in ℋ$
31 ffvelrn ${⊢}\left({U}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {U}\left({x}\right)\in ℋ$
32 31 ad2ant2lr ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {U}\left({x}\right)\in ℋ$
33 simprr ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {y}\in ℋ$
34 ax-his2 ${⊢}\left({T}\left({x}\right)\in ℋ\wedge {U}\left({x}\right)\in ℋ\wedge {y}\in ℋ\right)\to \left({T}\left({x}\right){+}_{ℎ}{U}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}=\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({U}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
35 30 32 33 34 syl3anc ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({T}\left({x}\right){+}_{ℎ}{U}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}=\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({U}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
36 28 35 eqtrd ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}=\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({U}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
37 11 36 sylan ${⊢}\left(\left({T}\in \mathrm{HrmOp}\wedge {U}\in \mathrm{HrmOp}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}=\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)+\left({U}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
38 10 24 37 3eqtr4d ${⊢}\left(\left({T}\in \mathrm{HrmOp}\wedge {U}\in \mathrm{HrmOp}\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}\left({T}{+}_{\mathrm{op}}{U}\right)\left({y}\right)=\left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
39 38 ralrimivva ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {U}\in \mathrm{HrmOp}\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}\left({T}{+}_{\mathrm{op}}{U}\right)\left({y}\right)=\left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
40 elhmop ${⊢}{T}{+}_{\mathrm{op}}{U}\in \mathrm{HrmOp}↔\left(\left({T}{+}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}\left({T}{+}_{\mathrm{op}}{U}\right)\left({y}\right)=\left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
41 4 39 40 sylanbrc ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {U}\in \mathrm{HrmOp}\right)\to {T}{+}_{\mathrm{op}}{U}\in \mathrm{HrmOp}$