cnvunopt - Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem cnvunopt 9781

Description: The inverse (converse) of a unitary operator in Hilbert space is unitary. Theorem in [AkhiezerGlazman] p. 72.

**Assertion**
Ref	Expression
cnvunopt	⊢ (T ∈ UniOp → ^◡T ∈ UniOp)

**Proof of Theorem cnvunopt**
Step	Hyp	Ref	Expression
1		unopf1ot 9779	. . . 4 ⊢ (T ∈ UniOp → T: ℋ –1-1-onto→ ℋ )
2		f1ocnv 3692	. . . . 5 ⊢ (T: ℋ –1-1-onto→ ℋ → ^◡T: ℋ –1-1-onto→ ℋ )
3		f1ofo 3686	. . . . 5 ⊢ (^◡T: ℋ –1-1-onto→ ℋ → ^◡T: ℋ –onto→ ℋ )
4	2, 3	syl 10	. . . 4 ⊢ (T: ℋ –1-1-onto→ ℋ → ^◡T: ℋ –onto→ ℋ )
5	1, 4	syl 10	. . 3 ⊢ (T ∈ UniOp → ^◡T: ℋ –onto→ ℋ )
6		unopt 9778	. . . . . . 7 ⊢ ((T ∈ UniOp ⋀ (^◡T ‘x) ∈ ℋ ⋀ (^◡T ‘y) ∈ ℋ ) → ((T ‘(^◡T ‘x)) ·_ih (T ‘(^◡T ‘y))) = ((^◡T ‘x) ·_ih (^◡T ‘y)))
7		pm3.26 319	. . . . . . 7 ⊢ ((T ∈ UniOp ⋀ (x ∈ ℋ ⋀ y ∈ ℋ )) → T ∈ UniOp)
8		ffvelrn 3805	. . . . . . . . 9 ⊢ ((^◡T: ℋ –→ ℋ ⋀ x ∈ ℋ ) → (^◡T ‘x) ∈ ℋ )
9		fof 3663	. . . . . . . . . 10 ⊢ (^◡T: ℋ –onto→ ℋ → ^◡T: ℋ –→ ℋ )
10	5, 9	syl 10	. . . . . . . . 9 ⊢ (T ∈ UniOp → ^◡T: ℋ –→ ℋ )
11	8, 10	sylan 448	. . . . . . . 8 ⊢ ((T ∈ UniOp ⋀ x ∈ ℋ ) → (^◡T ‘x) ∈ ℋ )
12	11	adantrr 395	. . . . . . 7 ⊢ ((T ∈ UniOp ⋀ (x ∈ ℋ ⋀ y ∈ ℋ )) → (^◡T ‘x) ∈ ℋ )
13		ffvelrn 3805	. . . . . . . . 9 ⊢ ((^◡T: ℋ –→ ℋ ⋀ y ∈ ℋ ) → (^◡T ‘y) ∈ ℋ )
14	13, 10	sylan 448	. . . . . . . 8 ⊢ ((T ∈ UniOp ⋀ y ∈ ℋ ) → (^◡T ‘y) ∈ ℋ )
15	14	adantrl 394	. . . . . . 7 ⊢ ((T ∈ UniOp ⋀ (x ∈ ℋ ⋀ y ∈ ℋ )) → (^◡T ‘y) ∈ ℋ )
16	6, 7, 12, 15	syl3anc 857	. . . . . 6 ⊢ ((T ∈ UniOp ⋀ (x ∈ ℋ ⋀ y ∈ ℋ )) → ((T ‘(^◡T ‘x)) ·_ih (T ‘(^◡T ‘y))) = ((^◡T ‘x) ·_ih (^◡T ‘y)))
17		f1ocnvfv2 3870	. . . . . . . . 9 ⊢ ((T: ℋ –1-1-onto→ ℋ ⋀ x ∈ ℋ ) → (T ‘(^◡T ‘x)) = x)
18	17	adantrr 395	. . . . . . . 8 ⊢ ((T: ℋ –1-1-onto→ ℋ ⋀ (x ∈ ℋ ⋀ y ∈ ℋ )) → (T ‘(^◡T ‘x)) = x)
19		f1ocnvfv2 3870	. . . . . . . . 9 ⊢ ((T: ℋ –1-1-onto→ ℋ ⋀ y ∈ ℋ ) → (T ‘(^◡T ‘y)) = y)
20	19	adantrl 394	. . . . . . . 8 ⊢ ((T: ℋ –1-1-onto→ ℋ ⋀ (x ∈ ℋ ⋀ y ∈ ℋ )) → (T ‘(^◡T ‘y)) = y)
21	18, 20	opreq12d 3969	. . . . . . 7 ⊢ ((T: ℋ –1-1-onto→ ℋ ⋀ (x ∈ ℋ ⋀ y ∈ ℋ )) → ((T ‘(^◡T ‘x)) ·_ih (T ‘(^◡T ‘y))) = (x ·_ih y))
22	21, 1	sylan 448	. . . . . 6 ⊢ ((T ∈ UniOp ⋀ (x ∈ ℋ ⋀ y ∈ ℋ )) → ((T ‘(^◡T ‘x)) ·_ih (T ‘(^◡T ‘y))) = (x ·_ih y))
23	16, 22	eqtr3d 1506	. . . . 5 ⊢ ((T ∈ UniOp ⋀ (x ∈ ℋ ⋀ y ∈ ℋ )) → ((^◡T ‘x) ·_ih (^◡T ‘y)) = (x ·_ih y))
24	23	ex 373	. . . 4 ⊢ (T ∈ UniOp → ((x ∈ ℋ ⋀ y ∈ ℋ ) → ((^◡T ‘x) ·_ih (^◡T ‘y)) = (x ·_ih y)))
25	24	r19.21aivv 1717	. . 3 ⊢ (T ∈ UniOp → ∀x ∈ ℋ ∀y ∈ ℋ ((^◡T ‘x) ·_ih (^◡T ‘y)) = (x ·_ih y))
26	5, 25	jca 288	. 2 ⊢ (T ∈ UniOp → (^◡T: ℋ –onto→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℋ ((^◡T ‘x) ·_ih (^◡T ‘y)) = (x ·_ih y)))
27		elunopt 9739	. 2 ⊢ (^◡T ∈ UniOp ↔ (^◡T: ℋ –onto→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℋ ((^◡T ‘x) ·_ih (^◡T ‘y)) = (x ·_ih y)))
28	26, 27	sylibr 200	1 ⊢ (T ∈ UniOp → ^◡T ∈ UniOp)

Colors of variables: wff set class

Syntax hints: → wi 3 ⋀ wa 223 = wceq 954 ∈ wcel 956 ∀wral 1642 ^◡ccnv 3164 –→wf 3173 –onto→wfo 3175 –1-1-onto→wf1o 3176 ‘cfv 3177 (class class class)co 3954 ℋ chil 8727 ·_ih csp 8732 UniOpcuo 8757

This theorem is referenced by: unoplint 9783 unopadj2t 9801

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-9 963 ax-10 964 ax-11 965 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-rep 2688 ax-sep 2698 ax-nul 2705 ax-pow 2737 ax-pr 2774 ax-un 2861 ax-inf2 4605 ax-hilex 8808 ax-hfvadd 8809 ax-hvcom 8810 ax-hvass 8811 ax-hv0cl 8812 ax-hvaddid 8813 ax-hfvmul 8814 ax-hvmulid 8815 ax-hvdistr2 8818 ax-hvmul0 8819 ax-hfi 8885 ax-his1 8888 ax-his2 8889 ax-his3 8890 ax-his4 8891

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 775 df-3an 776 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-nel 1585 df-ral 1646 df-rex 1647 df-reu 1648 df-rab 1649 df-v 1808 df-sbc 1938 df-csb 1998 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-pss 2051 df-nul 2277 df-if 2358 df-pw 2398 df-sn 2408 df-pr 2409 df-tp 2411 df-op 2412 df-uni 2499 df-int 2529 df-iun 2563 df-br 2615 df-opab 2662 df-tr 2676 df-eprel 2827 df-id 2830 df-po 2835 df-so 2845 df-fr 2912 df-we 2929 df-ord 2946 df-on 2947 df-lim 2948 df-suc 2949 df-om 3127 df-xp 3179 df-rel 3180 df-cnv 3181 df-co 3182 df-dm 3183 df-rn 3184 df-res 3185 df-ima 3186 df-fun 3187 df-fn 3188 df-f 3189 df-f1 3190 df-fo 3191 df-f1o 3192 df-fv 3193 df-rdg 3923 df-opr 3956 df-oprab 3957 df-1st 4069 df-2nd 4070 df-1o 4123 df-oadd 4125 df-omul 4126 df-er 4251 df-ec 4253 df-qs 4256 df-en 4357 df-dom 4358 df-sdom 4359 df-ni 4980 df-pli 4981 df-mi 4982 df-lti 4983 df-plpq 5015 df-mpq 5016 df-enq 5017 df-nq 5018 df-plq 5019 df-mq 5020 df-rq 5021 df-ltq 5022 df-1q 5023 df-np 5066 df-1p 5067 df-plp 5068 df-mp 5069 df-ltp 5070 df-plpr 5144 df-mpr 5145 df-enr 5146 df-nr 5147 df-plr 5148 df-mr 5149 df-ltr 5150 df-0r 5151 df-1r 5152 df-m1r 5153 df-c 5220 df-0 5221 df-1 5222 df-i 5223 df-r 5224 df-plus 5225 df-mul 5226 df-lt 5227 df-sub 5336 df-neg 5338 df-pnf 5467 df-mnf 5468 df-xr 5469 df-ltxr 5470 df-le 5471 df-div 5680 df-re 6690 df-im 6691 df-cj 6692 df-hvsub 8779 df-unop 9709