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 32005

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 31856	. . . 4 ⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶ ℋ)
2		hmopf 31856	. . . 4 ⊢ (𝑈 ∈ HrmOp → 𝑈: ℋ⟶ ℋ)
3		fco 6680	. . . 4 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 ∘ 𝑈): ℋ⟶ ℋ)
4	1, 2, 3	syl2an 596	. . 3 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 ∘ 𝑈): ℋ⟶ ℋ)
5	4	3adant3 1132	. 2 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (𝑇 ∘ 𝑈): ℋ⟶ ℋ)
6		fvco3 6927	. . . . . . . . . 10 ⊢ ((𝑈: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇 ∘ 𝑈)‘𝑦) = (𝑇‘(𝑈‘𝑦)))
7	2, 6	sylan 580	. . . . . . . . 9 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → ((𝑇 ∘ 𝑈)‘𝑦) = (𝑇‘(𝑈‘𝑦)))
8	7	oveq2d 7368	. . . . . . . 8 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))))
9	8	ad2ant2l 746	. . . . . . 7 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))))
10		simpll 766	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑇 ∈ HrmOp)
11		simprl 770	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑥 ∈ ℋ)
12	2	ffvelcdmda 7023	. . . . . . . . 9 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → (𝑈‘𝑦) ∈ ℋ)
13	12	ad2ant2l 746	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑈‘𝑦) ∈ ℋ)
14		hmop 31904	. . . . . . . 8 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ∧ (𝑈‘𝑦) ∈ ℋ) → (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))) = ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)))
15	10, 11, 13, 14	syl3anc 1373	. . . . . . 7 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))) = ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)))
16		simplr 768	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑈 ∈ HrmOp)
17	1	ffvelcdmda 7023	. . . . . . . . 9 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) ∈ ℋ)
18	17	ad2ant2r 747	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑇‘𝑥) ∈ ℋ)
19		simprr 772	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑦 ∈ ℋ)
20		hmop 31904	. . . . . . . 8 ⊢ ((𝑈 ∈ HrmOp ∧ (𝑇‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
21	16, 18, 19, 20	syl3anc 1373	. . . . . . 7 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
22	9, 15, 21	3eqtrd 2772	. . . . . 6 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
23		fvco3 6927	. . . . . . . . 9 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → ((𝑈 ∘ 𝑇)‘𝑥) = (𝑈‘(𝑇‘𝑥)))
24	1, 23	sylan 580	. . . . . . . 8 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ) → ((𝑈 ∘ 𝑇)‘𝑥) = (𝑈‘(𝑇‘𝑥)))
25	24	oveq1d 7367	. . . . . . 7 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ) → (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
26	25	ad2ant2r 747	. . . . . 6 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
27	22, 26	eqtr4d 2771	. . . . 5 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
28	27	3adantl3 1169	. . . 4 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
29		fveq1 6827	. . . . . . 7 ⊢ ((𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇) → ((𝑇 ∘ 𝑈)‘𝑥) = ((𝑈 ∘ 𝑇)‘𝑥))
30	29	oveq1d 7367	. . . . . 6 ⊢ ((𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇) → (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
31	30	3ad2ant3 1135	. . . . 5 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
32	31	adantr 480	. . . 4 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
33	28, 32	eqtr4d 2771	. . 3 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦))
34	33	ralrimivva 3176	. 2 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦))
35		elhmop 31855	. 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 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ∀wral 3048 ∘ ccom 5623 ⟶wf 6482 ‘cfv 6486 (class class class)co 7352 ℋchba 30901 ·_ih csp 30904 HrmOpcho 30932

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 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-hilex 30981

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-ral 3049 df-rex 3058 df-rab 3397 df-v 3439 df-sbc 3738 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-br 5094 df-opab 5156 df-id 5514 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-fv 6494 df-ov 7355 df-oprab 7356 df-mpo 7357 df-map 8758 df-hmop 31826

This theorem is referenced by: leopsq 32111 opsqrlem4 32125 opsqrlem6 32127

W3C validator