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 29806

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 29657	. . . 4 ⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶ ℋ)
2		hmopf 29657	. . . 4 ⊢ (𝑈 ∈ HrmOp → 𝑈: ℋ⟶ ℋ)
3		fco 6505	. . . 4 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 ∘ 𝑈): ℋ⟶ ℋ)
4	1, 2, 3	syl2an 598	. . 3 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 ∘ 𝑈): ℋ⟶ ℋ)
5	4	3adant3 1129	. 2 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (𝑇 ∘ 𝑈): ℋ⟶ ℋ)
6		fvco3 6737	. . . . . . . . . 10 ⊢ ((𝑈: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇 ∘ 𝑈)‘𝑦) = (𝑇‘(𝑈‘𝑦)))
7	2, 6	sylan 583	. . . . . . . . 9 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → ((𝑇 ∘ 𝑈)‘𝑦) = (𝑇‘(𝑈‘𝑦)))
8	7	oveq2d 7151	. . . . . . . 8 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))))
9	8	ad2ant2l 745	. . . . . . 7 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))))
10		simpll 766	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑇 ∈ HrmOp)
11		simprl 770	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑥 ∈ ℋ)
12	2	ffvelrnda 6828	. . . . . . . . 9 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → (𝑈‘𝑦) ∈ ℋ)
13	12	ad2ant2l 745	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑈‘𝑦) ∈ ℋ)
14		hmop 29705	. . . . . . . 8 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ∧ (𝑈‘𝑦) ∈ ℋ) → (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))) = ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)))
15	10, 11, 13, 14	syl3anc 1368	. . . . . . 7 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))) = ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)))
16		simplr 768	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑈 ∈ HrmOp)
17	1	ffvelrnda 6828	. . . . . . . . 9 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) ∈ ℋ)
18	17	ad2ant2r 746	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑇‘𝑥) ∈ ℋ)
19		simprr 772	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑦 ∈ ℋ)
20		hmop 29705	. . . . . . . 8 ⊢ ((𝑈 ∈ HrmOp ∧ (𝑇‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
21	16, 18, 19, 20	syl3anc 1368	. . . . . . 7 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
22	9, 15, 21	3eqtrd 2837	. . . . . 6 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
23		fvco3 6737	. . . . . . . . 9 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → ((𝑈 ∘ 𝑇)‘𝑥) = (𝑈‘(𝑇‘𝑥)))
24	1, 23	sylan 583	. . . . . . . 8 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ) → ((𝑈 ∘ 𝑇)‘𝑥) = (𝑈‘(𝑇‘𝑥)))
25	24	oveq1d 7150	. . . . . . 7 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ) → (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
26	25	ad2ant2r 746	. . . . . 6 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
27	22, 26	eqtr4d 2836	. . . . 5 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
28	27	3adantl3 1165	. . . 4 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
29		fveq1 6644	. . . . . . 7 ⊢ ((𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇) → ((𝑇 ∘ 𝑈)‘𝑥) = ((𝑈 ∘ 𝑇)‘𝑥))
30	29	oveq1d 7150	. . . . . 6 ⊢ ((𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇) → (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
31	30	3ad2ant3 1132	. . . . 5 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
32	31	adantr 484	. . . 4 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
33	28, 32	eqtr4d 2836	. . 3 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦))
34	33	ralrimivva 3156	. 2 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦))
35		elhmop 29656	. 2 ⊢ ((𝑇 ∘ 𝑈) ∈ HrmOp ↔ ((𝑇 ∘ 𝑈): ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦)))
36	5, 34, 35	sylanbrc 586	1 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (𝑇 ∘ 𝑈) ∈ HrmOp)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ∀wral 3106 ∘ ccom 5523 ⟶wf 6320 ‘cfv 6324 (class class class)co 7135 ℋchba 28702 ·_ih csp 28705 HrmOpcho 28733

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-hilex 28782

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-fv 6332 df-ov 7138 df-oprab 7139 df-mpo 7140 df-map 8391 df-hmop 29627

This theorem is referenced by: leopsq 29912 opsqrlem4 29926 opsqrlem6 29928

W3C validator