hmops - Hilbert Space Explorer

	Hilbert Space Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HSE Home > Th. List > hmops		Structured version Visualization version GIF version

Theorem hmops 30283

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

**Assertion**
Ref	Expression
hmops	⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 +_op 𝑈) ∈ HrmOp)

Proof of Theorem hmops Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hmopf 30137	. . 3 ⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶ ℋ)
2		hmopf 30137	. . 3 ⊢ (𝑈 ∈ HrmOp → 𝑈: ℋ⟶ ℋ)
3		hoaddcl 30021	. . 3 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 +_op 𝑈): ℋ⟶ ℋ)
4	1, 2, 3	syl2an 595	. 2 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 +_op 𝑈): ℋ⟶ ℋ)
5		hmop 30185	. . . . . . 7 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦))
6	5	3expb 1118	. . . . . 6 ⊢ ((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih (𝑇‘𝑦)) = ((𝑇‘𝑥) ·_ih 𝑦))
7		hmop 30185	. . . . . . 7 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 ·_ih (𝑈‘𝑦)) = ((𝑈‘𝑥) ·_ih 𝑦))
8	7	3expb 1118	. . . . . 6 ⊢ ((𝑈 ∈ HrmOp ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih (𝑈‘𝑦)) = ((𝑈‘𝑥) ·_ih 𝑦))
9	6, 8	oveqan12d 7274	. . . . 5 ⊢ (((𝑇 ∈ HrmOp ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) ∧ (𝑈 ∈ HrmOp ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ))) → ((𝑥 ·_ih (𝑇‘𝑦)) + (𝑥 ·_ih (𝑈‘𝑦))) = (((𝑇‘𝑥) ·_ih 𝑦) + ((𝑈‘𝑥) ·_ih 𝑦)))
10	9	anandirs 675	. . . 4 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑥 ·_ih (𝑇‘𝑦)) + (𝑥 ·_ih (𝑈‘𝑦))) = (((𝑇‘𝑥) ·_ih 𝑦) + ((𝑈‘𝑥) ·_ih 𝑦)))
11	1, 2	anim12i 612	. . . . 5 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ))
12		hosval 30003	. . . . . . . . 9 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇 +_op 𝑈)‘𝑦) = ((𝑇‘𝑦) +_ℎ (𝑈‘𝑦)))
13	12	oveq2d 7271	. . . . . . . 8 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 ·_ih ((𝑇 +_op 𝑈)‘𝑦)) = (𝑥 ·_ih ((𝑇‘𝑦) +_ℎ (𝑈‘𝑦))))
14	13	3expa 1116	. . . . . . 7 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) ∧ 𝑦 ∈ ℋ) → (𝑥 ·_ih ((𝑇 +_op 𝑈)‘𝑦)) = (𝑥 ·_ih ((𝑇‘𝑦) +_ℎ (𝑈‘𝑦))))
15	14	adantrl 712	. . . . . 6 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 +_op 𝑈)‘𝑦)) = (𝑥 ·_ih ((𝑇‘𝑦) +_ℎ (𝑈‘𝑦))))
16		simprl 767	. . . . . . 7 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑥 ∈ ℋ)
17		ffvelrn 6941	. . . . . . . 8 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) → (𝑇‘𝑦) ∈ ℋ)
18	17	ad2ant2rl 745	. . . . . . 7 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑇‘𝑦) ∈ ℋ)
19		ffvelrn 6941	. . . . . . . 8 ⊢ ((𝑈: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) → (𝑈‘𝑦) ∈ ℋ)
20	19	ad2ant2l 742	. . . . . . 7 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑈‘𝑦) ∈ ℋ)
21		his7 29353	. . . . . . 7 ⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑦) ∈ ℋ ∧ (𝑈‘𝑦) ∈ ℋ) → (𝑥 ·_ih ((𝑇‘𝑦) +_ℎ (𝑈‘𝑦))) = ((𝑥 ·_ih (𝑇‘𝑦)) + (𝑥 ·_ih (𝑈‘𝑦))))
22	16, 18, 20, 21	syl3anc 1369	. . . . . 6 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇‘𝑦) +_ℎ (𝑈‘𝑦))) = ((𝑥 ·_ih (𝑇‘𝑦)) + (𝑥 ·_ih (𝑈‘𝑦))))
23	15, 22	eqtrd 2778	. . . . 5 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 +_op 𝑈)‘𝑦)) = ((𝑥 ·_ih (𝑇‘𝑦)) + (𝑥 ·_ih (𝑈‘𝑦))))
24	11, 23	sylan 579	. . . 4 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 +_op 𝑈)‘𝑦)) = ((𝑥 ·_ih (𝑇‘𝑦)) + (𝑥 ·_ih (𝑈‘𝑦))))
25		hosval 30003	. . . . . . . . 9 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → ((𝑇 +_op 𝑈)‘𝑥) = ((𝑇‘𝑥) +_ℎ (𝑈‘𝑥)))
26	25	oveq1d 7270	. . . . . . . 8 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → (((𝑇 +_op 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑇‘𝑥) +_ℎ (𝑈‘𝑥)) ·_ih 𝑦))
27	26	3expa 1116	. . . . . . 7 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) → (((𝑇 +_op 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑇‘𝑥) +_ℎ (𝑈‘𝑥)) ·_ih 𝑦))
28	27	adantrr 713	. . . . . 6 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑇 +_op 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑇‘𝑥) +_ℎ (𝑈‘𝑥)) ·_ih 𝑦))
29		ffvelrn 6941	. . . . . . . 8 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) ∈ ℋ)
30	29	ad2ant2r 743	. . . . . . 7 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑇‘𝑥) ∈ ℋ)
31		ffvelrn 6941	. . . . . . . 8 ⊢ ((𝑈: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → (𝑈‘𝑥) ∈ ℋ)
32	31	ad2ant2lr 744	. . . . . . 7 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑈‘𝑥) ∈ ℋ)
33		simprr 769	. . . . . . 7 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑦 ∈ ℋ)
34		ax-his2 29346	. . . . . . 7 ⊢ (((𝑇‘𝑥) ∈ ℋ ∧ (𝑈‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑇‘𝑥) +_ℎ (𝑈‘𝑥)) ·_ih 𝑦) = (((𝑇‘𝑥) ·_ih 𝑦) + ((𝑈‘𝑥) ·_ih 𝑦)))
35	30, 32, 33, 34	syl3anc 1369	. . . . . 6 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑇‘𝑥) +_ℎ (𝑈‘𝑥)) ·_ih 𝑦) = (((𝑇‘𝑥) ·_ih 𝑦) + ((𝑈‘𝑥) ·_ih 𝑦)))
36	28, 35	eqtrd 2778	. . . . 5 ⊢ (((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑇 +_op 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑇‘𝑥) ·_ih 𝑦) + ((𝑈‘𝑥) ·_ih 𝑦)))
37	11, 36	sylan 579	. . . 4 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑇 +_op 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑇‘𝑥) ·_ih 𝑦) + ((𝑈‘𝑥) ·_ih 𝑦)))
38	10, 24, 37	3eqtr4d 2788	. . 3 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 +_op 𝑈)‘𝑦)) = (((𝑇 +_op 𝑈)‘𝑥) ·_ih 𝑦))
39	38	ralrimivva 3114	. 2 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih ((𝑇 +_op 𝑈)‘𝑦)) = (((𝑇 +_op 𝑈)‘𝑥) ·_ih 𝑦))
40		elhmop 30136	. 2 ⊢ ((𝑇 +_op 𝑈) ∈ HrmOp ↔ ((𝑇 +_op 𝑈): ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih ((𝑇 +_op 𝑈)‘𝑦)) = (((𝑇 +_op 𝑈)‘𝑥) ·_ih 𝑦)))
41	4, 39, 40	sylanbrc 582	1 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 +_op 𝑈) ∈ HrmOp)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ∀wral 3063 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 + caddc 10805 ℋchba 29182 +_ℎ cva 29183 ·_ih csp 29185 +_op chos 29201 HrmOpcho 29213

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-hilex 29262 ax-hfvadd 29263 ax-hfi 29342 ax-his1 29345 ax-his2 29346

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-po 5494 df-so 5495 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-2 11966 df-cj 14738 df-re 14739 df-im 14740 df-hosum 29993 df-hmop 30107

This theorem is referenced by: hmopd 30285 leopadd 30395 opsqrlem4 30406

W3C validator