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 30494

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 30345	. . . 4 ⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶ ℋ)
2		hmopf 30345	. . . 4 ⊢ (𝑈 ∈ HrmOp → 𝑈: ℋ⟶ ℋ)
3		fco 6661	. . . 4 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 ∘ 𝑈): ℋ⟶ ℋ)
4	1, 2, 3	syl2an 596	. . 3 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 ∘ 𝑈): ℋ⟶ ℋ)
5	4	3adant3 1131	. 2 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (𝑇 ∘ 𝑈): ℋ⟶ ℋ)
6		fvco3 6906	. . . . . . . . . 10 ⊢ ((𝑈: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇 ∘ 𝑈)‘𝑦) = (𝑇‘(𝑈‘𝑦)))
7	2, 6	sylan 580	. . . . . . . . 9 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → ((𝑇 ∘ 𝑈)‘𝑦) = (𝑇‘(𝑈‘𝑦)))
8	7	oveq2d 7331	. . . . . . . 8 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))))
9	8	ad2ant2l 743	. . . . . . 7 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))))
10		simpll 764	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑇 ∈ HrmOp)
11		simprl 768	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑥 ∈ ℋ)
12	2	ffvelcdmda 7000	. . . . . . . . 9 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → (𝑈‘𝑦) ∈ ℋ)
13	12	ad2ant2l 743	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑈‘𝑦) ∈ ℋ)
14		hmop 30393	. . . . . . . 8 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ∧ (𝑈‘𝑦) ∈ ℋ) → (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))) = ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)))
15	10, 11, 13, 14	syl3anc 1370	. . . . . . 7 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))) = ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)))
16		simplr 766	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑈 ∈ HrmOp)
17	1	ffvelcdmda 7000	. . . . . . . . 9 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) ∈ ℋ)
18	17	ad2ant2r 744	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑇‘𝑥) ∈ ℋ)
19		simprr 770	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑦 ∈ ℋ)
20		hmop 30393	. . . . . . . 8 ⊢ ((𝑈 ∈ HrmOp ∧ (𝑇‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
21	16, 18, 19, 20	syl3anc 1370	. . . . . . 7 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
22	9, 15, 21	3eqtrd 2781	. . . . . 6 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
23		fvco3 6906	. . . . . . . . 9 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → ((𝑈 ∘ 𝑇)‘𝑥) = (𝑈‘(𝑇‘𝑥)))
24	1, 23	sylan 580	. . . . . . . 8 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ) → ((𝑈 ∘ 𝑇)‘𝑥) = (𝑈‘(𝑇‘𝑥)))
25	24	oveq1d 7330	. . . . . . 7 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ) → (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
26	25	ad2ant2r 744	. . . . . 6 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
27	22, 26	eqtr4d 2780	. . . . 5 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
28	27	3adantl3 1167	. . . 4 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
29		fveq1 6810	. . . . . . 7 ⊢ ((𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇) → ((𝑇 ∘ 𝑈)‘𝑥) = ((𝑈 ∘ 𝑇)‘𝑥))
30	29	oveq1d 7330	. . . . . 6 ⊢ ((𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇) → (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
31	30	3ad2ant3 1134	. . . . 5 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
32	31	adantr 481	. . . 4 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
33	28, 32	eqtr4d 2780	. . 3 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦))
34	33	ralrimivva 3194	. 2 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦))
35		elhmop 30344	. 2 ⊢ ((𝑇 ∘ 𝑈) ∈ HrmOp ↔ ((𝑇 ∘ 𝑈): ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦)))
36	5, 34, 35	sylanbrc 583	1 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (𝑇 ∘ 𝑈) ∈ HrmOp)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ∀wral 3062 ∘ ccom 5611 ⟶wf 6461 ‘cfv 6465 (class class class)co 7315 ℋchba 29390 ·_ih csp 29393 HrmOpcho 29421

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2708 ax-sep 5238 ax-nul 5245 ax-pow 5303 ax-pr 5367 ax-un 7628 ax-hilex 29470

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3405 df-v 3443 df-sbc 3727 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4268 df-if 4472 df-pw 4547 df-sn 4572 df-pr 4574 df-op 4578 df-uni 4851 df-br 5088 df-opab 5150 df-id 5507 df-xp 5613 df-rel 5614 df-cnv 5615 df-co 5616 df-dm 5617 df-rn 5618 df-res 5619 df-ima 5620 df-iota 6417 df-fun 6467 df-fn 6468 df-f 6469 df-fv 6473 df-ov 7318 df-oprab 7319 df-mpo 7320 df-map 8665 df-hmop 30315

This theorem is referenced by: leopsq 30600 opsqrlem4 30614 opsqrlem6 30616

W3C validator