cnvadj - Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem cnvadj 10096

Description: The adjoint function equals its converse.

**Assertion**
Ref	Expression
cnvadj	⊢ ^◡adj_h = adj_h

**Proof of Theorem cnvadj**
Step	Hyp	Ref	Expression
1		cnvopab 3537	. . 3 ⊢ ^◡{u, t∣(u: ℋ –→ ℋ ⋀ t: ℋ –→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y))} = {t, u∣(u: ℋ –→ ℋ ⋀ t: ℋ –→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y))}
2		3ancoma 788	. . . . 5 ⊢ ((u: ℋ –→ ℋ ⋀ t: ℋ –→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y)) ↔ (t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y)))
3		ax-his1 9225	. . . . . . . . . . . . . . . . . 18 ⊢ (((u ‘y) ∈ ℋ ⋀ x ∈ ℋ ) → ((u ‘y) ·_ih x) = (∗ ‘(x ·_ih (u ‘y))))
4		ffvelrn 3928	. . . . . . . . . . . . . . . . . 18 ⊢ ((u: ℋ –→ ℋ ⋀ y ∈ ℋ ) → (u ‘y) ∈ ℋ )
5	3, 4	sylan 450	. . . . . . . . . . . . . . . . 17 ⊢ (((u: ℋ –→ ℋ ⋀ y ∈ ℋ ) ⋀ x ∈ ℋ ) → ((u ‘y) ·_ih x) = (∗ ‘(x ·_ih (u ‘y))))
6	5	adantrl 394	. . . . . . . . . . . . . . . 16 ⊢ (((u: ℋ –→ ℋ ⋀ y ∈ ℋ ) ⋀ (t: ℋ –→ ℋ ⋀ x ∈ ℋ )) → ((u ‘y) ·_ih x) = (∗ ‘(x ·_ih (u ‘y))))
7		ax-his1 9225	. . . . . . . . . . . . . . . . . 18 ⊢ ((y ∈ ℋ ⋀ (t ‘x) ∈ ℋ ) → (y ·_ih (t ‘x)) = (∗ ‘((t ‘x) ·_ih y)))
8		ffvelrn 3928	. . . . . . . . . . . . . . . . . 18 ⊢ ((t: ℋ –→ ℋ ⋀ x ∈ ℋ ) → (t ‘x) ∈ ℋ )
9	7, 8	sylan2 453	. . . . . . . . . . . . . . . . 17 ⊢ ((y ∈ ℋ ⋀ (t: ℋ –→ ℋ ⋀ x ∈ ℋ )) → (y ·_ih (t ‘x)) = (∗ ‘((t ‘x) ·_ih y)))
10	9	adantll 392	. . . . . . . . . . . . . . . 16 ⊢ (((u: ℋ –→ ℋ ⋀ y ∈ ℋ ) ⋀ (t: ℋ –→ ℋ ⋀ x ∈ ℋ )) → (y ·_ih (t ‘x)) = (∗ ‘((t ‘x) ·_ih y)))
11	6, 10	eqeq12d 1532	. . . . . . . . . . . . . . 15 ⊢ (((u: ℋ –→ ℋ ⋀ y ∈ ℋ ) ⋀ (t: ℋ –→ ℋ ⋀ x ∈ ℋ )) → (((u ‘y) ·_ih x) = (y ·_ih (t ‘x)) ↔ (∗ ‘(x ·_ih (u ‘y))) = (∗ ‘((t ‘x) ·_ih y))))
12	11	ancoms 438	. . . . . . . . . . . . . 14 ⊢ (((t: ℋ –→ ℋ ⋀ x ∈ ℋ ) ⋀ (u: ℋ –→ ℋ ⋀ y ∈ ℋ )) → (((u ‘y) ·_ih x) = (y ·_ih (t ‘x)) ↔ (∗ ‘(x ·_ih (u ‘y))) = (∗ ‘((t ‘x) ·_ih y))))
13		cj11 7031	. . . . . . . . . . . . . . 15 ⊢ (((x ·_ih (u ‘y)) ∈ ℂ ⋀ ((t ‘x) ·_ih y) ∈ ℂ) → ((∗ ‘(x ·_ih (u ‘y))) = (∗ ‘((t ‘x) ·_ih y)) ↔ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y)))
14		hicl 9223	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ ℋ ⋀ (u ‘y) ∈ ℋ ) → (x ·_ih (u ‘y)) ∈ ℂ)
15	14, 4	sylan2 453	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ ℋ ⋀ (u: ℋ –→ ℋ ⋀ y ∈ ℋ )) → (x ·_ih (u ‘y)) ∈ ℂ)
16	15	adantll 392	. . . . . . . . . . . . . . 15 ⊢ (((t: ℋ –→ ℋ ⋀ x ∈ ℋ ) ⋀ (u: ℋ –→ ℋ ⋀ y ∈ ℋ )) → (x ·_ih (u ‘y)) ∈ ℂ)
17		hicl 9223	. . . . . . . . . . . . . . . . 17 ⊢ (((t ‘x) ∈ ℋ ⋀ y ∈ ℋ ) → ((t ‘x) ·_ih y) ∈ ℂ)
18	17, 8	sylan 450	. . . . . . . . . . . . . . . 16 ⊢ (((t: ℋ –→ ℋ ⋀ x ∈ ℋ ) ⋀ y ∈ ℋ ) → ((t ‘x) ·_ih y) ∈ ℂ)
19	18	adantrl 394	. . . . . . . . . . . . . . 15 ⊢ (((t: ℋ –→ ℋ ⋀ x ∈ ℋ ) ⋀ (u: ℋ –→ ℋ ⋀ y ∈ ℋ )) → ((t ‘x) ·_ih y) ∈ ℂ)
20	13, 16, 19	sylanc 473	. . . . . . . . . . . . . 14 ⊢ (((t: ℋ –→ ℋ ⋀ x ∈ ℋ ) ⋀ (u: ℋ –→ ℋ ⋀ y ∈ ℋ )) → ((∗ ‘(x ·_ih (u ‘y))) = (∗ ‘((t ‘x) ·_ih y)) ↔ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y)))
21	12, 20	bitr2d 532	. . . . . . . . . . . . 13 ⊢ (((t: ℋ –→ ℋ ⋀ x ∈ ℋ ) ⋀ (u: ℋ –→ ℋ ⋀ y ∈ ℋ )) → ((x ·_ih (u ‘y)) = ((t ‘x) ·_ih y) ↔ ((u ‘y) ·_ih x) = (y ·_ih (t ‘x))))
22	21	an4s 511	. . . . . . . . . . . 12 ⊢ (((t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ) ⋀ (x ∈ ℋ ⋀ y ∈ ℋ )) → ((x ·_ih (u ‘y)) = ((t ‘x) ·_ih y) ↔ ((u ‘y) ·_ih x) = (y ·_ih (t ‘x))))
23	22	anassrs 443	. . . . . . . . . . 11 ⊢ ((((t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ) ⋀ x ∈ ℋ ) ⋀ y ∈ ℋ ) → ((x ·_ih (u ‘y)) = ((t ‘x) ·_ih y) ↔ ((u ‘y) ·_ih x) = (y ·_ih (t ‘x))))
24		eqcom 1520	. . . . . . . . . . 11 ⊢ (((u ‘y) ·_ih x) = (y ·_ih (t ‘x)) ↔ (y ·_ih (t ‘x)) = ((u ‘y) ·_ih x))
25	23, 24	syl6bb 539	. . . . . . . . . 10 ⊢ ((((t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ) ⋀ x ∈ ℋ ) ⋀ y ∈ ℋ ) → ((x ·_ih (u ‘y)) = ((t ‘x) ·_ih y) ↔ (y ·_ih (t ‘x)) = ((u ‘y) ·_ih x)))
26	25	ralbidva 1705	. . . . . . . . 9 ⊢ (((t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ) ⋀ x ∈ ℋ ) → (∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y) ↔ ∀y ∈ ℋ (y ·_ih (t ‘x)) = ((u ‘y) ·_ih x)))
27	26	ralbidva 1705	. . . . . . . 8 ⊢ ((t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ) → (∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y) ↔ ∀x ∈ ℋ ∀y ∈ ℋ (y ·_ih (t ‘x)) = ((u ‘y) ·_ih x)))
28		ralcom 1820	. . . . . . . 8 ⊢ (∀x ∈ ℋ ∀y ∈ ℋ (y ·_ih (t ‘x)) = ((u ‘y) ·_ih x) ↔ ∀y ∈ ℋ ∀x ∈ ℋ (y ·_ih (t ‘x)) = ((u ‘y) ·_ih x))
29	27, 28	syl6bb 539	. . . . . . 7 ⊢ ((t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ) → (∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y) ↔ ∀y ∈ ℋ ∀x ∈ ℋ (y ·_ih (t ‘x)) = ((u ‘y) ·_ih x)))
30	29	pm5.32i 648	. . . . . 6 ⊢ (((t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ) ⋀ ∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y)) ↔ ((t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ) ⋀ ∀y ∈ ℋ ∀x ∈ ℋ (y ·_ih (t ‘x)) = ((u ‘y) ·_ih x)))
31		df-3an 783	. . . . . 6 ⊢ ((t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y)) ↔ ((t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ) ⋀ ∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y)))
32		df-3an 783	. . . . . 6 ⊢ ((t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ⋀ ∀y ∈ ℋ ∀x ∈ ℋ (y ·_ih (t ‘x)) = ((u ‘y) ·_ih x)) ↔ ((t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ) ⋀ ∀y ∈ ℋ ∀x ∈ ℋ (y ·_ih (t ‘x)) = ((u ‘y) ·_ih x)))
33	30, 31, 32	3bitr4i 181	. . . . 5 ⊢ ((t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y)) ↔ (t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ⋀ ∀y ∈ ℋ ∀x ∈ ℋ (y ·_ih (t ‘x)) = ((u ‘y) ·_ih x)))
34	2, 33	bitri 171	. . . 4 ⊢ ((u: ℋ –→ ℋ ⋀ t: ℋ –→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y)) ↔ (t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ⋀ ∀y ∈ ℋ ∀x ∈ ℋ (y ·_ih (t ‘x)) = ((u ‘y) ·_ih x)))
35	34	opabbii 2745	. . 3 ⊢ {t, u∣(u: ℋ –→ ℋ ⋀ t: ℋ –→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y))} = {t, u∣(t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ⋀ ∀y ∈ ℋ ∀x ∈ ℋ (y ·_ih (t ‘x)) = ((u ‘y) ·_ih x))}
36	1, 35	eqtri 1538	. 2 ⊢ ^◡{u, t∣(u: ℋ –→ ℋ ⋀ t: ℋ –→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y))} = {t, u∣(t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ⋀ ∀y ∈ ℋ ∀x ∈ ℋ (y ·_ih (t ‘x)) = ((u ‘y) ·_ih x))}
37		dfadj2 10092	. . 3 ⊢ adj_h = {u, t∣(u: ℋ –→ ℋ ⋀ t: ℋ –→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y))}
38	37	cnveqi 3383	. 2 ⊢ ^◡adj_h = ^◡{u, t∣(u: ℋ –→ ℋ ⋀ t: ℋ –→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (u ‘y)) = ((t ‘x) ·_ih y))}
39		dfadj2 10092	. 2 ⊢ adj_h = {t, u∣(t: ℋ –→ ℋ ⋀ u: ℋ –→ ℋ ⋀ ∀y ∈ ℋ ∀x ∈ ℋ (y ·_ih (t ‘x)) = ((u ‘y) ·_ih x))}
40	36, 38, 39	3eqtr4i 1548	1 ⊢ ^◡adj_h = adj_h

Colors of variables: wff set class

Syntax hints: ↔ wb 144 ⋀ wa 221 ⋀ w3a 781 = wceq 992 ∈ wcel 994 ∀wral 1691 {copab 2740 ^◡ccnv 3250 –→wf 3259 ‘cfv 3263 (class class class)co 4021 ℂcc 5386 ∗ccj 6950 ℋ chil 9063 ·_ih csp 9068 adj_hcado 9099

This theorem is referenced by: funcnvadj 10097 adj1o 10098 adjbdlnb 10296

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 998 ax-gen 999 ax-8 1000 ax-9 1001 ax-10 1002 ax-11 1003 ax-12 1004 ax-13 1005 ax-14 1006 ax-17 1007 ax-4 1009 ax-5o 1011 ax-6o 1014 ax-9o 1159 ax-10o 1177 ax-16 1247 ax-11o 1255 ax-ext 1500 ax-rep 2767 ax-sep 2777 ax-nul 2784 ax-pow 2818 ax-pr 2855 ax-un 3089 ax-inf2 4770 ax-hfi 9222 ax-his1 9225

This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 782 df-3an 783 df-ex 1017 df-sb 1209 df-eu 1421 df-mo 1422 df-clab 1506 df-cleq 1511 df-clel 1514 df-ne 1630 df-nel 1631 df-ral 1695 df-rex 1696 df-reu 1697 df-rab 1698 df-v 1858 df-sbc 1987 df-csb 2052 df-dif 2101 df-un 2102 df-in 2103 df-ss 2105 df-pss 2107 df-nul 2333 df-if 2416 df-pw 2459 df-sn 2470 df-pr 2471 df-tp 2473 df-op 2474 df-uni 2570 df-int 2601 df-iun 2635 df-br 2693 df-opab 2741 df-tr 2755 df-eprel 2910 df-id 2913 df-po 2918 df-so 2929 df-fr 2947 df-we 2962 df-ord 2978 df-on 2979 df-lim 2980 df-suc 2981 df-om 3219 df-xp 3265 df-rel 3266 df-cnv 3267 df-co 3268 df-dm 3269 df-rn 3270 df-res 3271 df-ima 3272 df-fun 3273 df-fn 3274 df-f 3275 df-f1 3276 df-fo 3277 df-f1o 3278 df-fv 3279 df-opr 4023 df-oprab 4024 df-1st 4140 df-2nd 4141 df-rdg 4233 df-1o 4269 df-oadd 4271 df-omul 4272 df-er 4401 df-ec 4403 df-qs 4406 df-en 4509 df-dom 4510 df-sdom 4511 df-ni 5154 df-pli 5155 df-mi 5156 df-lti 5157 df-plpq 5189 df-mpq 5190 df-enq 5191 df-nq 5192 df-plq 5193 df-mq 5194 df-rq 5195 df-ltq 5196 df-1q 5197 df-np 5240 df-1p 5241 df-plp 5242 df-mp 5243 df-ltp 5244 df-plpr 5318 df-mpr 5319 df-enr 5320 df-nr 5321 df-plr 5322 df-mr 5323 df-ltr 5324 df-0r 5325 df-1r 5326 df-m1r 5327 df-c 5394 df-0 5395 df-1 5396 df-i 5397 df-r 5398 df-plus 5399 df-mul 5400 df-lt 5401 df-sub 5510 df-neg 5512 df-pnf 5641 df-mnf 5642 df-xr 5643 df-ltxr 5644 df-le 5645 df-div 5855 df-re 6952 df-im 6953 df-cj 6954 df-adjh 10055