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 ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → T + op U ∈ HrmOp

Proof

Step Hyp Ref Expression
1 hmopf ⊢ T ∈ HrmOp → T : ℋ ⟶ ℋ
2 hmopf ⊢ U ∈ HrmOp → U : ℋ ⟶ ℋ
3 hoaddcl ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ → T + op U : ℋ ⟶ ℋ
4 1 2 3 syl2an ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → T + op U : ℋ ⟶ ℋ
5 hmop ⊢ T ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
6 5 3expb ⊢ T ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
7 hmop ⊢ U ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih U ⁡ y = U ⁡ x ⋅ ih y
8 7 3expb ⊢ U ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih U ⁡ y = U ⁡ x ⋅ ih y
9 6 8 oveqan12d ⊢ T ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ ∧ U ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y + x ⋅ ih U ⁡ y = T ⁡ x ⋅ ih y + U ⁡ x ⋅ ih y
10 9 anandirs ⊢ T ∈ HrmOp ∧ U ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y + x ⋅ ih U ⁡ y = T ⁡ x ⋅ ih y + U ⁡ x ⋅ ih y
11 1 2 anim12i ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ
12 hosval ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ y ∈ ℋ → T + op U ⁡ y = T ⁡ y + ℎ U ⁡ y
13 12 oveq2d ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ y ∈ ℋ → x ⋅ ih T + op U ⁡ y = x ⋅ ih T ⁡ y + ℎ U ⁡ y
14 13 3expa ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ y ∈ ℋ → x ⋅ ih T + op U ⁡ y = x ⋅ ih T ⁡ y + ℎ U ⁡ y
15 14 adantrl ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T + op U ⁡ y = x ⋅ ih T ⁡ y + ℎ U ⁡ y
16 simprl ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → x ∈ ℋ
17 ffvelrn ⊢ T : ℋ ⟶ ℋ ∧ y ∈ ℋ → T ⁡ y ∈ ℋ
18 17 ad2ant2rl ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ y ∈ ℋ
19 ffvelrn ⊢ U : ℋ ⟶ ℋ ∧ y ∈ ℋ → U ⁡ y ∈ ℋ
20 19 ad2ant2l ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → U ⁡ y ∈ ℋ
21 his7 ⊢ x ∈ ℋ ∧ T ⁡ y ∈ ℋ ∧ U ⁡ y ∈ ℋ → x ⋅ ih T ⁡ y + ℎ U ⁡ y = x ⋅ ih T ⁡ y + x ⋅ ih U ⁡ y
22 16 18 20 21 syl3anc ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y + ℎ U ⁡ y = x ⋅ ih T ⁡ y + x ⋅ ih U ⁡ y
23 15 22 eqtrd ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T + op U ⁡ y = x ⋅ ih T ⁡ y + x ⋅ ih U ⁡ y
24 11 23 sylan ⊢ T ∈ HrmOp ∧ U ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T + op U ⁡ y = x ⋅ ih T ⁡ y + x ⋅ ih U ⁡ y
25 hosval ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ → T + op U ⁡ x = T ⁡ x + ℎ U ⁡ x
26 25 oveq1d ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ → T + op U ⁡ x ⋅ ih y = T ⁡ x + ℎ U ⁡ x ⋅ ih y
27 26 3expa ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ → T + op U ⁡ x ⋅ ih y = T ⁡ x + ℎ U ⁡ x ⋅ ih y
28 27 adantrr ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → T + op U ⁡ x ⋅ ih y = T ⁡ x + ℎ U ⁡ x ⋅ ih y
29 ffvelrn ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → T ⁡ x ∈ ℋ
30 29 ad2ant2r ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ∈ ℋ
31 ffvelrn ⊢ U : ℋ ⟶ ℋ ∧ x ∈ ℋ → U ⁡ x ∈ ℋ
32 31 ad2ant2lr ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → U ⁡ x ∈ ℋ
33 simprr ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → y ∈ ℋ
34 ax-his2 ⊢ T ⁡ x ∈ ℋ ∧ U ⁡ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x + ℎ U ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y + U ⁡ x ⋅ ih y
35 30 32 33 34 syl3anc ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x + ℎ U ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y + U ⁡ x ⋅ ih y
36 28 35 eqtrd ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ y ∈ ℋ → T + op U ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y + U ⁡ x ⋅ ih y
37 11 36 sylan ⊢ T ∈ HrmOp ∧ U ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → T + op U ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y + U ⁡ x ⋅ ih y
38 10 24 37 3eqtr4d ⊢ T ∈ HrmOp ∧ U ∈ HrmOp ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T + op U ⁡ y = T + op U ⁡ x ⋅ ih y
39 38 ralrimivva ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T + op U ⁡ y = T + op U ⁡ x ⋅ ih y
40 elhmop ⊢ T + op U ∈ HrmOp ↔ T + op U : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T + op U ⁡ y = T + op U ⁡ x ⋅ ih y
41 4 39 40 sylanbrc ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → T + op U ∈ HrmOp