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 32631

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 32482	. . . 4 ⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶ ℋ)
2		hmopf 32482	. . . 4 ⊢ (𝑈 ∈ HrmOp → 𝑈: ℋ⟶ ℋ)
3		fco 6735	. . . 4 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑈: ℋ⟶ ℋ) → (𝑇 ∘ 𝑈): ℋ⟶ ℋ)
4	1, 2, 3	syl2an 608	. . 3 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) → (𝑇 ∘ 𝑈): ℋ⟶ ℋ)
5	4	3adant3 1150	. 2 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (𝑇 ∘ 𝑈): ℋ⟶ ℋ)
6		fvco3 6986	. . . . . . . . . 10 ⊢ ((𝑈: ℋ⟶ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇 ∘ 𝑈)‘𝑦) = (𝑇‘(𝑈‘𝑦)))
7	2, 6	sylan 592	. . . . . . . . 9 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → ((𝑇 ∘ 𝑈)‘𝑦) = (𝑇‘(𝑈‘𝑦)))
8	7	oveq2d 7437	. . . . . . . 8 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))))
9	8	ad2ant2l 759	. . . . . . 7 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))))
10		simpll 779	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑇 ∈ HrmOp)
11		simprl 783	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑥 ∈ ℋ)
12	2	ffvelcdmda 7085	. . . . . . . . 9 ⊢ ((𝑈 ∈ HrmOp ∧ 𝑦 ∈ ℋ) → (𝑈‘𝑦) ∈ ℋ)
13	12	ad2ant2l 759	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑈‘𝑦) ∈ ℋ)
14		hmop 32530	. . . . . . . 8 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ∧ (𝑈‘𝑦) ∈ ℋ) → (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))) = ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)))
15	10, 11, 13, 14	syl3anc 1398	. . . . . . 7 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih (𝑇‘(𝑈‘𝑦))) = ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)))
16		simplr 781	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑈 ∈ HrmOp)
17	1	ffvelcdmda 7085	. . . . . . . . 9 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) ∈ ℋ)
18	17	ad2ant2r 760	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑇‘𝑥) ∈ ℋ)
19		simprr 785	. . . . . . . 8 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → 𝑦 ∈ ℋ)
20		hmop 32530	. . . . . . . 8 ⊢ ((𝑈 ∈ HrmOp ∧ (𝑇‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
21	16, 18, 19, 20	syl3anc 1398	. . . . . . 7 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → ((𝑇‘𝑥) ·_ih (𝑈‘𝑦)) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
22	9, 15, 21	3eqtrd 2799	. . . . . 6 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
23		fvco3 6986	. . . . . . . . 9 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → ((𝑈 ∘ 𝑇)‘𝑥) = (𝑈‘(𝑇‘𝑥)))
24	1, 23	sylan 592	. . . . . . . 8 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ) → ((𝑈 ∘ 𝑇)‘𝑥) = (𝑈‘(𝑇‘𝑥)))
25	24	oveq1d 7436	. . . . . . 7 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ) → (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
26	25	ad2ant2r 760	. . . . . 6 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦) = ((𝑈‘(𝑇‘𝑥)) ·_ih 𝑦))
27	22, 26	eqtr4d 2798	. . . . 5 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
28	27	3adantl3 1187	. . . 4 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
29		fveq1 6885	. . . . . . 7 ⊢ ((𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇) → ((𝑇 ∘ 𝑈)‘𝑥) = ((𝑈 ∘ 𝑇)‘𝑥))
30	29	oveq1d 7436	. . . . . 6 ⊢ ((𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇) → (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
31	30	3ad2ant3 1153	. . . . 5 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
32	31	adantr 486	. . . 4 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦) = (((𝑈 ∘ 𝑇)‘𝑥) ·_ih 𝑦))
33	28, 32	eqtr4d 2798	. . 3 ⊢ (((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦))
34	33	ralrimivva 3205	. 2 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦))
35		elhmop 32481	. 2 ⊢ ((𝑇 ∘ 𝑈) ∈ HrmOp ↔ ((𝑇 ∘ 𝑈): ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·_ih ((𝑇 ∘ 𝑈)‘𝑦)) = (((𝑇 ∘ 𝑈)‘𝑥) ·_ih 𝑦)))
36	5, 34, 35	sylanbrc 595	1 ⊢ ((𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ∧ (𝑇 ∘ 𝑈) = (𝑈 ∘ 𝑇)) → (𝑇 ∘ 𝑈) ∈ HrmOp)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∀wral 3076 ∘ ccom 5654 ⟶wf 6535 ‘cfv 6539 (class class class)co 7421 ℋchba 31527 ·_ih csp 31530 HrmOpcho 31558

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-hilex 31607

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-sbc 3739 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-br 5103 df-opab 5167 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-fv 6547 df-ov 7424 df-oprab 7425 df-mpo 7426 df-map 8853 df-hmop 32452

This theorem is used by: leopsq 32737 opsqrlem4 32751 opsqrlem6 32753

W3C validator