Theorem adjbdlnt 10016

Description: The adjoint of a bounded linear operator is a bounded linear operator.

Assertion

Ref	Expression
adjbdlnt	|- (T e. BndLinOp -> (adjh` T) e. BndLinOp)

Proof of Theorem adjbdlnt

Step	Hyp	Ref	Expression
1		df-rab 1652	. . . . . 6 |- {t e. (H~ ^m H~) | A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))} = {t | (t e. (H~ ^m H~) /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))}
2		ax-hilex 8869	. . . . . . . . 9 |- H~ e. V
3	2, 2	elmap 4334	. . . . . . . 8 |- (t e. (H~ ^m H~) <-> t:H~-->H~)
4	3	anbi1i 481	. . . . . . 7 |- ((t e. (H~ ^m H~) /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))) <-> (t:H~-->H~ /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))))
5	4	abbii 1575	. . . . . 6 |- {t | (t e. (H~ ^m H~) /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))} = {t | (t:H~-->H~ /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))}
6	1, 5	eqtr 1495	. . . . 5 |- {t e. (H~ ^m H~) | A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))} = {t | (t:H~-->H~ /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))}
7	6	unieqi 2511	. . . 4 |- U.{t e. (H~ ^m H~) | A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))} = U.{t | (t:H~-->H~ /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))}
8	7	a1i 8	. . 3 |- (T e. BndLinOp -> U.{t e. (H~ ^m H~) | A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))} = U.{t | (t:H~-->H~ /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))})
9		bdopft 9789	. . . . . . 7 |- (t e. BndLinOp -> t:H~-->H~)
10	9, 3	sylibr 200	. . . . . 6 |- (t e. BndLinOp -> t e. (H~ ^m H~))
11	10	ssriv 2069	. . . . 5 |- BndLinOp (_ (H~ ^m H~)
12		mouniss 2890	. . . . 5 |- ((BndLinOp (_ (H~ ^m H~) /\ E.t e. BndLinOp A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)) /\ E*t(t e. (H~ ^m H~) /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))) -> U.{t e. BndLinOp | A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))} = U.{t e. (H~ ^m H~) | A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))})
13	11, 12	mp3an1 903	. . . 4 |- ((E.t e. BndLinOp A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)) /\ E*t(t e. (H~ ^m H~) /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))) -> U.{t e. BndLinOp | A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))} = U.{t e. (H~ ^m H~) | A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))})
14		cnlnadjt 10012	. . . . 5 |- (T e. (LinOp i^i ConOp) -> E.t e. (LinOp i^i ConOp)A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))
15		lncnopbd 9966	. . . . 5 |- (T e. (LinOp i^i ConOp) <-> T e. BndLinOp)
16		lncnbd 9967	. . . . . 6 |- (LinOp i^i ConOp) = BndLinOp
17		rexeq1 1787	. . . . . 6 |- ((LinOp i^i ConOp) = BndLinOp -> (E.t e. (LinOp i^i ConOp)A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)) <-> E.t e. BndLinOp A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))))
18	16, 17	ax-mp 7	. . . . 5 |- (E.t e. (LinOp i^i ConOp)A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)) <-> E.t e. BndLinOp A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))
19	14, 15, 18	3imtr3 218	. . . 4 |- (T e. BndLinOp -> E.t e. BndLinOp A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))
20		adjmo 9758	. . . . 5 |- E*t(t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (T` y)) = ((t` x) .ih y))
21		ax-17 971	. . . . . 6 |- (T e. BndLinOp -> A.t T e. BndLinOp)
22		adjsymt 9759	. . . . . . . . 9 |- ((T:H~-->H~ /\ t:H~-->H~) -> (A.x e. H~ A.y e. H~ (x .ih (T` y)) = ((t` x) .ih y) <-> A.x e. H~ A.y e. H~ (x .ih (t` y)) = ((T` x) .ih y)))
23		bdopft 9789	. . . . . . . . 9 |- (T e. BndLinOp -> T:H~-->H~)
24	22, 23	sylan 448	. . . . . . . 8 |- ((T e. BndLinOp /\ t:H~-->H~) -> (A.x e. H~ A.y e. H~ (x .ih (T` y)) = ((t` x) .ih y) <-> A.x e. H~ A.y e. H~ (x .ih (t` y)) = ((T` x) .ih y)))
25	24	pm5.32da 649	. . . . . . 7 |- (T e. BndLinOp -> ((t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (T` y)) = ((t` x) .ih y)) <-> (t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (t` y)) = ((T` x) .ih y))))
26		eqcom 1477	. . . . . . . . 9 |- (((T` x) .ih y) = (x .ih (t` y)) <-> (x .ih (t` y)) = ((T` x) .ih y))
27	26	2ralbii 1669	. . . . . . . 8 |- (A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)) <-> A.x e. H~ A.y e. H~ (x .ih (t` y)) = ((T` x) .ih y))
28	3, 27	anbi12i 482	. . . . . . 7 |- ((t e. (H~ ^m H~) /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))) <-> (t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (t` y)) = ((T` x) .ih y)))
29	25, 28	syl6rbbr 539	. . . . . 6 |- (T e. BndLinOp -> ((t e. (H~ ^m H~) /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))) <-> (t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (T` y)) = ((t` x) .ih y))))
30	21, 29	mobid 1404	. . . . 5 |- (T e. BndLinOp -> (E*t(t e. (H~ ^m H~) /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))) <-> E*t(t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (T` y)) = ((t` x) .ih y))))
31	20, 30	mpbiri 194	. . . 4 |- (T e. BndLinOp -> E*t(t e. (H~ ^m H~) /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))))
32	13, 19, 31	sylanc 471	. . 3 |- (T e. BndLinOp -> U.{t e. BndLinOp | A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))} = U.{t e. (H~ ^m H~) | A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))})
33		adjval2t 9815	. . . 4 |- (T:H~-->H~ -> (adjh` T) = U.{t | (t:H~-->H~ /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))})
34	23, 33	syl 10	. . 3 |- (T e. BndLinOp -> (adjh` T) = U.{t | (t:H~-->H~ /\ A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))})
35	8, 32, 34	3eqtr4rd 1518	. 2 |- (T e. BndLinOp -> (adjh` T) = U.{t e. BndLinOp | A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))})
36		cnlnadjeut 10011	. . . 4 |- (T e. (LinOp i^i ConOp) -> E!t e. (LinOp i^i ConOp)A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)))
37		reueq1 1788	. . . . 5 |- ((LinOp i^i ConOp) = BndLinOp -> (E!t e. (LinOp i^i ConOp)A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y)) <-> E!t e. BndLinOp A.x e. H~ A.y e. H~ ((T` x) .ih y) = (x .ih (t` y))))
38