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 ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 +op 𝑈 ) ∈ HrmOp )

Proof

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