hmopco - Hilbert Space Explorer

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

Theorem hmopco 32284

Description: The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006.) (New usage is discouraged.)

**Assertion**
Ref	Expression
hmopco	⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (𝑇 ∘ 𝑈) ∈ HrmOp)

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

Step	Hyp	Ref	Expression
1		hmopf 32135	. . . 4 ⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶ ℋ)
2		hmopf 32135	. . . 4 ⊢ (𝑈 ∈ HrmOp → 𝑈: ℋ⟶ ℋ)
3		fco 6720	. . . 4 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 ∘ 𝑈): ℋ⟶ ℋ)
4	1, 2, 3	syl2an 607	. . 3 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 ∘ 𝑈): ℋ⟶ ℋ)
5	4	3adant3 1148	. 2 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (𝑇 ∘ 𝑈): ℋ⟶ ℋ)
6		fvco3 6971	. . . . . . . . . 10 ⊢ ((𝑈: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇 ∘ 𝑈)‘𝑦) = (𝑇‘(𝑈‘𝑦)))
7	2, 6	sylan 591	. . . . . . . . 9 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → ((𝑇 ∘ 𝑈)‘𝑦) = (𝑇‘(𝑈‘𝑦)))
8	7	oveq2d 7416	. . . . . . . 8 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))))
9	8	ad2ant2l 758	. . . . . . 7 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))))
10		simpll 778	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑇 ∈ HrmOp)
11		simprl 782	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑥 ∈ ℋ)
12	2	ffvelcdmda 7069	. . . . . . . . 9 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → (𝑈‘𝑦) ∈ ℋ)
13	12	ad2ant2l 758	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑈‘𝑦) ∈ ℋ)
14		hmop 32183	. . . . . . . 8 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ∧ (𝑈‘𝑦) ∈ ℋ) → (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))) = ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)))
15	10, 11, 13, 14	syl3anc 1394	. . . . . . 7 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))) = ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)))
16		simplr 780	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑈 ∈ HrmOp)
17	1	ffvelcdmda 7069	. . . . . . . . 9 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) ∈ ℋ)
18	17	ad2ant2r 759	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑇‘𝑥) ∈ ℋ)
19		simprr 784	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑦 ∈ ℋ)
20		hmop 32183	. . . . . . . 8 ⊢ ((𝑈 ∈ HrmOp ∧ (𝑇‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
21	16, 18, 19, 20	syl3anc 1394	. . . . . . 7 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
22	9, 15, 21	3eqtrd 2804	. . . . . 6 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
23		fvco3 6971	. . . . . . . . 9 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → ((𝑈 ∘ 𝑇)‘𝑥) = (𝑈‘(𝑇‘𝑥)))
24	1, 23	sylan 591	. . . . . . . 8 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ) → ((𝑈 ∘ 𝑇)‘𝑥) = (𝑈‘(𝑇‘𝑥)))
25	24	oveq1d 7415	. . . . . . 7 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ) → (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
26	25	ad2ant2r 759	. . . . . 6 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
27	22, 26	eqtr4d 2803	. . . . 5 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
28	27	3adantl3 1185	. . . 4 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
29		fveq1 6870	. . . . . . 7 ⊢ ((𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇) → ((𝑇 ∘ 𝑈)‘𝑥) = ((𝑈 ∘ 𝑇)‘𝑥))
30	29	oveq1d 7415	. . . . . 6 ⊢ ((𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇) → (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
31	30	3ad2ant3 1151	. . . . 5 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
32	31	adantr 485	. . . 4 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
33	28, 32	eqtr4d 2803	. . 3 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦))
34	33	ralrimivva 3208	. 2 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦))
35		elhmop 32134	. 2 ⊢ ((𝑇 ∘ 𝑈) ∈ HrmOp ↔ ((𝑇 ∘ 𝑈): ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦)))
36	5, 34, 35	sylanbrc 594	1 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (𝑇 ∘ 𝑈) ∈ HrmOp)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ∀wral 3079 ∘ ccom 5656 ⟶wf 6521 ‘cfv 6525 (class class class)co 7400 ℋchba 31180 ·_ih csp 31183 HrmOpcho 31211

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-hilex 31260

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-sbc 3748 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-br 5106 df-opab 5168 df-id 5547 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-fv 6533 df-ov 7403 df-oprab 7404 df-mpo 7405 df-map 8814 df-hmop 32105

This theorem is referenced by: leopsq 32390 opsqrlem4 32404 opsqrlem6 32406

W3C validator