Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > adjcoi | Structured version Visualization version GIF version |
Description: The adjoint of a composition of bounded linear operators. Theorem 3.11(viii) of [Beran] p. 106. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nmoptri.1 | ⊢ 𝑆 ∈ BndLinOp |
nmoptri.2 | ⊢ 𝑇 ∈ BndLinOp |
Ref | Expression |
---|---|
adjcoi | ⊢ (adjℎ‘(𝑆 ∘ 𝑇)) = ((adjℎ‘𝑇) ∘ (adjℎ‘𝑆)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nmoptri.2 | . . . . . . . 8 ⊢ 𝑇 ∈ BndLinOp | |
2 | adjbdln 30018 | . . . . . . . 8 ⊢ (𝑇 ∈ BndLinOp → (adjℎ‘𝑇) ∈ BndLinOp) | |
3 | bdopf 29797 | . . . . . . . 8 ⊢ ((adjℎ‘𝑇) ∈ BndLinOp → (adjℎ‘𝑇): ℋ⟶ ℋ) | |
4 | 1, 2, 3 | mp2b 10 | . . . . . . 7 ⊢ (adjℎ‘𝑇): ℋ⟶ ℋ |
5 | nmoptri.1 | . . . . . . . 8 ⊢ 𝑆 ∈ BndLinOp | |
6 | adjbdln 30018 | . . . . . . . 8 ⊢ (𝑆 ∈ BndLinOp → (adjℎ‘𝑆) ∈ BndLinOp) | |
7 | bdopf 29797 | . . . . . . . 8 ⊢ ((adjℎ‘𝑆) ∈ BndLinOp → (adjℎ‘𝑆): ℋ⟶ ℋ) | |
8 | 5, 6, 7 | mp2b 10 | . . . . . . 7 ⊢ (adjℎ‘𝑆): ℋ⟶ ℋ |
9 | 4, 8 | hocoi 29699 | . . . . . 6 ⊢ (𝑦 ∈ ℋ → (((adjℎ‘𝑇) ∘ (adjℎ‘𝑆))‘𝑦) = ((adjℎ‘𝑇)‘((adjℎ‘𝑆)‘𝑦))) |
10 | 9 | oveq2d 7187 | . . . . 5 ⊢ (𝑦 ∈ ℋ → (𝑥 ·ih (((adjℎ‘𝑇) ∘ (adjℎ‘𝑆))‘𝑦)) = (𝑥 ·ih ((adjℎ‘𝑇)‘((adjℎ‘𝑆)‘𝑦)))) |
11 | 10 | adantl 485 | . . . 4 ⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 ·ih (((adjℎ‘𝑇) ∘ (adjℎ‘𝑆))‘𝑦)) = (𝑥 ·ih ((adjℎ‘𝑇)‘((adjℎ‘𝑆)‘𝑦)))) |
12 | bdopf 29797 | . . . . . . . . 9 ⊢ (𝑆 ∈ BndLinOp → 𝑆: ℋ⟶ ℋ) | |
13 | 5, 12 | ax-mp 5 | . . . . . . . 8 ⊢ 𝑆: ℋ⟶ ℋ |
14 | bdopf 29797 | . . . . . . . . 9 ⊢ (𝑇 ∈ BndLinOp → 𝑇: ℋ⟶ ℋ) | |
15 | 1, 14 | ax-mp 5 | . . . . . . . 8 ⊢ 𝑇: ℋ⟶ ℋ |
16 | 13, 15 | hocoi 29699 | . . . . . . 7 ⊢ (𝑥 ∈ ℋ → ((𝑆 ∘ 𝑇)‘𝑥) = (𝑆‘(𝑇‘𝑥))) |
17 | 16 | oveq1d 7186 | . . . . . 6 ⊢ (𝑥 ∈ ℋ → (((𝑆 ∘ 𝑇)‘𝑥) ·ih 𝑦) = ((𝑆‘(𝑇‘𝑥)) ·ih 𝑦)) |
18 | 17 | adantr 484 | . . . . 5 ⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑆 ∘ 𝑇)‘𝑥) ·ih 𝑦) = ((𝑆‘(𝑇‘𝑥)) ·ih 𝑦)) |
19 | 15 | ffvelrni 6861 | . . . . . 6 ⊢ (𝑥 ∈ ℋ → (𝑇‘𝑥) ∈ ℋ) |
20 | bdopadj 30017 | . . . . . . . 8 ⊢ (𝑆 ∈ BndLinOp → 𝑆 ∈ dom adjℎ) | |
21 | 5, 20 | ax-mp 5 | . . . . . . 7 ⊢ 𝑆 ∈ dom adjℎ |
22 | adj2 29869 | . . . . . . 7 ⊢ ((𝑆 ∈ dom adjℎ ∧ (𝑇‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑆‘(𝑇‘𝑥)) ·ih 𝑦) = ((𝑇‘𝑥) ·ih ((adjℎ‘𝑆)‘𝑦))) | |
23 | 21, 22 | mp3an1 1449 | . . . . . 6 ⊢ (((𝑇‘𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑆‘(𝑇‘𝑥)) ·ih 𝑦) = ((𝑇‘𝑥) ·ih ((adjℎ‘𝑆)‘𝑦))) |
24 | 19, 23 | sylan 583 | . . . . 5 ⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑆‘(𝑇‘𝑥)) ·ih 𝑦) = ((𝑇‘𝑥) ·ih ((adjℎ‘𝑆)‘𝑦))) |
25 | 8 | ffvelrni 6861 | . . . . . 6 ⊢ (𝑦 ∈ ℋ → ((adjℎ‘𝑆)‘𝑦) ∈ ℋ) |
26 | bdopadj 30017 | . . . . . . . 8 ⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ dom adjℎ) | |
27 | 1, 26 | ax-mp 5 | . . . . . . 7 ⊢ 𝑇 ∈ dom adjℎ |
28 | adj2 29869 | . . . . . . 7 ⊢ ((𝑇 ∈ dom adjℎ ∧ 𝑥 ∈ ℋ ∧ ((adjℎ‘𝑆)‘𝑦) ∈ ℋ) → ((𝑇‘𝑥) ·ih ((adjℎ‘𝑆)‘𝑦)) = (𝑥 ·ih ((adjℎ‘𝑇)‘((adjℎ‘𝑆)‘𝑦)))) | |
29 | 27, 28 | mp3an1 1449 | . . . . . 6 ⊢ ((𝑥 ∈ ℋ ∧ ((adjℎ‘𝑆)‘𝑦) ∈ ℋ) → ((𝑇‘𝑥) ·ih ((adjℎ‘𝑆)‘𝑦)) = (𝑥 ·ih ((adjℎ‘𝑇)‘((adjℎ‘𝑆)‘𝑦)))) |
30 | 25, 29 | sylan2 596 | . . . . 5 ⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘𝑥) ·ih ((adjℎ‘𝑆)‘𝑦)) = (𝑥 ·ih ((adjℎ‘𝑇)‘((adjℎ‘𝑆)‘𝑦)))) |
31 | 18, 24, 30 | 3eqtrd 2777 | . . . 4 ⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑆 ∘ 𝑇)‘𝑥) ·ih 𝑦) = (𝑥 ·ih ((adjℎ‘𝑇)‘((adjℎ‘𝑆)‘𝑦)))) |
32 | 5, 1 | bdopcoi 30033 | . . . . . 6 ⊢ (𝑆 ∘ 𝑇) ∈ BndLinOp |
33 | bdopadj 30017 | . . . . . 6 ⊢ ((𝑆 ∘ 𝑇) ∈ BndLinOp → (𝑆 ∘ 𝑇) ∈ dom adjℎ) | |
34 | 32, 33 | ax-mp 5 | . . . . 5 ⊢ (𝑆 ∘ 𝑇) ∈ dom adjℎ |
35 | adj2 29869 | . . . . 5 ⊢ (((𝑆 ∘ 𝑇) ∈ dom adjℎ ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑆 ∘ 𝑇)‘𝑥) ·ih 𝑦) = (𝑥 ·ih ((adjℎ‘(𝑆 ∘ 𝑇))‘𝑦))) | |
36 | 34, 35 | mp3an1 1449 | . . . 4 ⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑆 ∘ 𝑇)‘𝑥) ·ih 𝑦) = (𝑥 ·ih ((adjℎ‘(𝑆 ∘ 𝑇))‘𝑦))) |
37 | 11, 31, 36 | 3eqtr2rd 2780 | . . 3 ⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 ·ih ((adjℎ‘(𝑆 ∘ 𝑇))‘𝑦)) = (𝑥 ·ih (((adjℎ‘𝑇) ∘ (adjℎ‘𝑆))‘𝑦))) |
38 | 37 | rgen2 3115 | . 2 ⊢ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih ((adjℎ‘(𝑆 ∘ 𝑇))‘𝑦)) = (𝑥 ·ih (((adjℎ‘𝑇) ∘ (adjℎ‘𝑆))‘𝑦)) |
39 | adjbdln 30018 | . . . 4 ⊢ ((𝑆 ∘ 𝑇) ∈ BndLinOp → (adjℎ‘(𝑆 ∘ 𝑇)) ∈ BndLinOp) | |
40 | bdopf 29797 | . . . 4 ⊢ ((adjℎ‘(𝑆 ∘ 𝑇)) ∈ BndLinOp → (adjℎ‘(𝑆 ∘ 𝑇)): ℋ⟶ ℋ) | |
41 | 32, 39, 40 | mp2b 10 | . . 3 ⊢ (adjℎ‘(𝑆 ∘ 𝑇)): ℋ⟶ ℋ |
42 | 4, 8 | hocofi 29701 | . . 3 ⊢ ((adjℎ‘𝑇) ∘ (adjℎ‘𝑆)): ℋ⟶ ℋ |
43 | hoeq2 29766 | . . 3 ⊢ (((adjℎ‘(𝑆 ∘ 𝑇)): ℋ⟶ ℋ ∧ ((adjℎ‘𝑇) ∘ (adjℎ‘𝑆)): ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih ((adjℎ‘(𝑆 ∘ 𝑇))‘𝑦)) = (𝑥 ·ih (((adjℎ‘𝑇) ∘ (adjℎ‘𝑆))‘𝑦)) ↔ (adjℎ‘(𝑆 ∘ 𝑇)) = ((adjℎ‘𝑇) ∘ (adjℎ‘𝑆)))) | |
44 | 41, 42, 43 | mp2an 692 | . 2 ⊢ (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih ((adjℎ‘(𝑆 ∘ 𝑇))‘𝑦)) = (𝑥 ·ih (((adjℎ‘𝑇) ∘ (adjℎ‘𝑆))‘𝑦)) ↔ (adjℎ‘(𝑆 ∘ 𝑇)) = ((adjℎ‘𝑇) ∘ (adjℎ‘𝑆))) |
45 | 38, 44 | mpbi 233 | 1 ⊢ (adjℎ‘(𝑆 ∘ 𝑇)) = ((adjℎ‘𝑇) ∘ (adjℎ‘𝑆)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 = wceq 1542 ∈ wcel 2113 ∀wral 3053 dom cdm 5526 ∘ ccom 5530 ⟶wf 6336 ‘cfv 6340 (class class class)co 7171 ℋchba 28854 ·ih csp 28857 BndLinOpcbo 28883 adjℎcado 28890 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-rep 5155 ax-sep 5168 ax-nul 5175 ax-pow 5233 ax-pr 5297 ax-un 7480 ax-inf2 9178 ax-cc 9936 ax-cnex 10672 ax-resscn 10673 ax-1cn 10674 ax-icn 10675 ax-addcl 10676 ax-addrcl 10677 ax-mulcl 10678 ax-mulrcl 10679 ax-mulcom 10680 ax-addass 10681 ax-mulass 10682 ax-distr 10683 ax-i2m1 10684 ax-1ne0 10685 ax-1rid 10686 ax-rnegex 10687 ax-rrecex 10688 ax-cnre 10689 ax-pre-lttri 10690 ax-pre-lttrn 10691 ax-pre-ltadd 10692 ax-pre-mulgt0 10693 ax-pre-sup 10694 ax-addf 10695 ax-mulf 10696 ax-hilex 28934 ax-hfvadd 28935 ax-hvcom 28936 ax-hvass 28937 ax-hv0cl 28938 ax-hvaddid 28939 ax-hfvmul 28940 ax-hvmulid 28941 ax-hvmulass 28942 ax-hvdistr1 28943 ax-hvdistr2 28944 ax-hvmul0 28945 ax-hfi 29014 ax-his1 29017 ax-his2 29018 ax-his3 29019 ax-his4 29020 ax-hcompl 29137 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3400 df-sbc 3683 df-csb 3792 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-pss 3863 df-nul 4213 df-if 4416 df-pw 4491 df-sn 4518 df-pr 4520 df-tp 4522 df-op 4524 df-uni 4798 df-int 4838 df-iun 4884 df-iin 4885 df-br 5032 df-opab 5094 df-mpt 5112 df-tr 5138 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5484 df-se 5485 df-we 5486 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-res 5538 df-ima 5539 df-pred 6130 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-isom 6349 df-riota 7128 df-ov 7174 df-oprab 7175 df-mpo 7176 df-of 7426 df-om 7601 df-1st 7715 df-2nd 7716 df-supp 7858 df-wrecs 7977 df-recs 8038 df-rdg 8076 df-1o 8132 df-2o 8133 df-oadd 8136 df-omul 8137 df-er 8321 df-map 8440 df-pm 8441 df-ixp 8509 df-en 8557 df-dom 8558 df-sdom 8559 df-fin 8560 df-fsupp 8908 df-fi 8949 df-sup 8980 df-inf 8981 df-oi 9048 df-card 9442 df-acn 9445 df-pnf 10756 df-mnf 10757 df-xr 10758 df-ltxr 10759 df-le 10760 df-sub 10951 df-neg 10952 df-div 11377 df-nn 11718 df-2 11780 df-3 11781 df-4 11782 df-5 11783 df-6 11784 df-7 11785 df-8 11786 df-9 11787 df-n0 11978 df-z 12064 df-dec 12181 df-uz 12326 df-q 12432 df-rp 12474 df-xneg 12591 df-xadd 12592 df-xmul 12593 df-ioo 12826 df-ico 12828 df-icc 12829 df-fz 12983 df-fzo 13126 df-fl 13254 df-seq 13462 df-exp 13523 df-hash 13784 df-cj 14549 df-re 14550 df-im 14551 df-sqrt 14685 df-abs 14686 df-clim 14936 df-rlim 14937 df-sum 15137 df-struct 16589 df-ndx 16590 df-slot 16591 df-base 16593 df-sets 16594 df-ress 16595 df-plusg 16682 df-mulr 16683 df-starv 16684 df-sca 16685 df-vsca 16686 df-ip 16687 df-tset 16688 df-ple 16689 df-ds 16691 df-unif 16692 df-hom 16693 df-cco 16694 df-rest 16800 df-topn 16801 df-0g 16819 df-gsum 16820 df-topgen 16821 df-pt 16822 df-prds 16825 df-xrs 16879 df-qtop 16884 df-imas 16885 df-xps 16887 df-mre 16961 df-mrc 16962 df-acs 16964 df-mgm 17969 df-sgrp 18018 df-mnd 18029 df-submnd 18074 df-mulg 18344 df-cntz 18566 df-cmn 19027 df-psmet 20210 df-xmet 20211 df-met 20212 df-bl 20213 df-mopn 20214 df-fbas 20215 df-fg 20216 df-cnfld 20219 df-top 21646 df-topon 21663 df-topsp 21685 df-bases 21698 df-cld 21771 df-ntr 21772 df-cls 21773 df-nei 21850 df-cn 21979 df-cnp 21980 df-lm 21981 df-t1 22066 df-haus 22067 df-tx 22314 df-hmeo 22507 df-fil 22598 df-fm 22690 df-flim 22691 df-flf 22692 df-xms 23074 df-ms 23075 df-tms 23076 df-cfil 24008 df-cau 24009 df-cmet 24010 df-grpo 28428 df-gid 28429 df-ginv 28430 df-gdiv 28431 df-ablo 28480 df-vc 28494 df-nv 28527 df-va 28530 df-ba 28531 df-sm 28532 df-0v 28533 df-vs 28534 df-nmcv 28535 df-ims 28536 df-dip 28636 df-ssp 28657 df-lno 28679 df-nmoo 28680 df-0o 28682 df-ph 28748 df-cbn 28798 df-hnorm 28903 df-hba 28904 df-hvsub 28906 df-hlim 28907 df-hcau 28908 df-sh 29142 df-ch 29156 df-oc 29187 df-ch0 29188 df-shs 29243 df-pjh 29330 df-h0op 29683 df-nmop 29774 df-cnop 29775 df-lnop 29776 df-bdop 29777 df-unop 29778 df-hmop 29779 df-nmfn 29780 df-nlfn 29781 df-cnfn 29782 df-lnfn 29783 df-adjh 29784 |
This theorem is referenced by: pjcmul1i 30136 |
Copyright terms: Public domain | W3C validator |