Theorem cnlnssadj 10013

Description: Every continuous linear Hilbert space operator has an adjoint.

Assertion

Ref	Expression
cnlnssadj	|- (LinOp i^i ConOp) (_ dom adjh

Proof of Theorem cnlnssadj

Step	Hyp	Ref	Expression
1		cnlnadjt 10012	. . . . 5 |- (y e. (LinOp i^i ConOp) -> E.t e. (LinOp i^i ConOp)A.x e. H~ A.z e. H~ ((y` x) .ih z) = (x .ih (t` z)))
2		df-rex 1650	. . . . 5 |- (E.t e. (LinOp i^i ConOp)A.x e. H~ A.z e. H~ ((y` x) .ih z) = (x .ih (t` z)) <-> E.t(t e. (LinOp i^i ConOp) /\ A.x e. H~ A.z e. H~ ((y` x) .ih z) = (x .ih (t` z))))
3	1, 2	sylib 198	. . . 4 |- (y e. (LinOp i^i ConOp) -> E.t(t e. (LinOp i^i ConOp) /\ A.x e. H~ A.z e. H~ ((y` x) .ih z) = (x .ih (t` z))))
4		inss1 2230	. . . . . . . . . 10 |- (LinOp i^i ConOp) (_ LinOp
5	4	sseli 2065	. . . . . . . . 9 |- (y e. (LinOp i^i ConOp) -> y e. LinOp)
6		lnopft 9785	. . . . . . . . 9 |- (y e. LinOp -> y:H~-->H~)
7	5, 6	syl 10	. . . . . . . 8 |- (y e. (LinOp i^i ConOp) -> y:H~-->H~)
8	7	a1d 12	. . . . . . 7 |- (y e. (LinOp i^i ConOp) -> ((t e. (LinOp i^i ConOp) /\ A.x e. H~ A.z e. H~ ((y` x) .ih z) = (x .ih (t` z))) -> y:H~-->H~))
9	4	sseli 2065	. . . . . . . . . 10 |- (t e. (LinOp i^i ConOp) -> t e. LinOp)
10		lnopft 9785	. . . . . . . . . 10 |- (t e. LinOp -> t:H~-->H~)
11	9, 10	syl 10	. . . . . . . . 9 |- (t e. (LinOp i^i ConOp) -> t:H~-->H~)
12	11	a1i 8	. . . . . . . 8 |- (y e. (LinOp i^i ConOp) -> (t e. (LinOp i^i ConOp) -> t:H~-->H~))
13	12	adantrd 391	. . . . . . 7 |- (y e. (LinOp i^i ConOp) -> ((t e. (LinOp i^i ConOp) /\ A.x e. H~ A.z e. H~ ((y` x) .ih z) = (x .ih (t` z))) -> t:H~-->H~))
14		adjsymt 9759	. . . . . . . . . . . 12 |- ((t:H~-->H~ /\ y:H~-->H~) -> (A.x e. H~ A.z e. H~ (x .ih (t` z)) = ((y` x) .ih z) <-> A.x e. H~ A.z e. H~ (x .ih (y` z)) = ((t` x) .ih z)))
15	14, 11, 7	syl2an 454	. . . . . . . . . . 11 |- ((t e. (LinOp i^i ConOp) /\ y e. (LinOp i^i ConOp)) -> (A.x e. H~ A.z e. H~ (x .ih (t` z)) = ((y` x) .ih z) <-> A.x e. H~ A.z e. H~ (x .ih (y` z)) = ((t` x) .ih z)))
16	15	ancoms 436	. . . . . . . . . 10 |- ((y e. (LinOp i^i ConOp) /\ t e. (LinOp i^i ConOp)) -> (A.x e. H~ A.z e. H~ (x .ih (t` z)) = ((y` x) .ih z) <-> A.x e. H~ A.z e. H~ (x .ih (y` z)) = ((t` x) .ih z)))
17		eqcom 1477	. . . . . . . . . . . . 13 |- (((y` x) .ih z) = (x .ih (t` z)) <-> (x .ih (t` z)) = ((y` x) .ih z))
18	17	biimp 151	. . . . . . . . . . . 12 |- (((y` x) .ih z) = (x .ih (t` z)) -> (x .ih (t` z)) = ((y` x) .ih z))
19	18	r19.20si 1706	. . . . . . . . . . 11 |- (A.z e. H~ ((y` x) .ih z) = (x .ih (t` z)) -> A.z e. H~ (x .ih (t` z)) = ((y` x) .ih z))
20	19	r19.20si 1706	. . . . . . . . . 10 |- (A.x e. H~ A.z e. H~ ((y` x) .ih z) = (x .ih (t` z)) -> A.x e. H~ A.z e. H~ (x .ih (t` z)) = ((y` x) .ih z))
21	16, 20	syl5bi 208	. . . . . . . . 9 |- ((y e. (LinOp i^i ConOp) /\ t e. (LinOp i^i ConOp)) -> (A.x e. H~ A.z e. H~ ((y` x) .ih z) = (x .ih (t` z)) -> A.x e. H~ A.z e. H~ (x .ih (y` z)) = ((t` x) .ih z)))
22	21	ex 373	. . . . . . . 8 |- (y e. (LinOp i^i ConOp) -> (t e. (LinOp i^i ConOp) -> (A.x e. H~ A.z e. H~ ((y` x) .ih z) = (x .ih (t` z)) -> A.x e. H~ A.z e. H~ (x .ih (y` z)) = ((t` x) .ih z))))
23	22	imp3a 361	. . . . . . 7 |- (y e. (LinOp i^i ConOp) -> ((t e. (LinOp i^i ConOp) /\ A.x e. H~ A.z e. H~ ((y` x) .ih z) = (x .ih (t` z))) -> A.x e. H~ A.z e. H~ (x .ih (y` z)) = ((t` x) .ih z)))
24	8, 13, 23	3jcad 820	. . . . . 6 |- (y e. (LinOp i^i ConOp) -> ((t e. (LinOp i^i ConOp) /\ A.x e. H~ A.z e. H~ ((y` x) .ih z) = (x .ih (t` z))) -> (y:H~-->H~ /\ t:H~-->H~ /\ A.x e. H~ A.z e. H~ (x .ih (y` z)) = ((t` x) .ih z))))
25		dfadj2 9812	. . . . . . . 8 |- adjh = {<.u, v>. | (u:H~-->H~ /\ v:H~-->H~ /\ A.x e. H~ A.z e. H~ (x .ih (u` z)) = ((v` x) .ih z))}
26	25	eleq2i 1538	. . . . . . 7 |- (<.y, t>. e. adjh <-> <.y, t>. e. {<.u, v>. | (u:H~-->H~ /\ v:H~-->H~ /\ A.x e. H~ A.z e. H~ (x .ih (u` z)) = ((v` x) .ih z))})
27		visset 1813	. . . . . . . 8 |- y e. V
28		visset 1813	. . . . . . . 8 |- t e. V
29		feq1 3620	. . . . . . . . 9 |- (u = y -> (u:H~-->H~ <-> y:H~-->H~))
30		fveq1 3723	. . . . . . . . . . . 12 |- (u = y -> (u` z) = (y` z))
31	30	opreq2d 3976	. . . . . . . . . . 11 |- (u = y -> (x .ih (u` z)) = (x .ih (y` z)))
32	31	eqeq1d 1483	. . . . . . . . . 10 |- (u = y -> ((x .ih (u` z)) = ((v` x) .ih z) <-> (x .ih (y` z)) = ((v` x) .ih z)))
33	32	2ralbidv 1680	. . . . . . . . 9 |- (u = y -> (A.x e. H~ A.z e. H~ (x .ih (u` z)) = ((v` x) .ih z) <-> A.x e. H~ A.z e. H~ (x .ih (y` z)) = ((v` x) .ih z)))
34	29, 33	3anbi13d 895	. . . . . . . 8 |- (u = y -> ((u:H~-->H~ /\ v:H~-->H~ /\ A.x e. H~ A.z e. H~ (x .ih (u` z)) = ((v` x) .ih z)) <-> (y:H~-->H~ /\ v:H~-->H~ /\ A.x e. H~ A.z e. H~ (x .ih (y` z)) = ((v` x) .ih z))))
35		feq1 3620	. . . . . . . . 9 |- (v = t -> (v:H~-->H~ <-> t:H~-->H~))
36		fveq1 3723	. . . . . . . . . . . 12 |- (v = t -> (v` x) = (t` x))
37	36	opreq1d 3975	. . . . . . . . . . 11 |- (v = t -> ((v` x) .ih z) = ((t` x) .ih z))
38	37	eqeq2d 1486	. . . . . . . . . 10 |- (v = t -> ((x .ih (y` z)) = ((v` x) .ih z) <-> (x .ih (y` z)) = ((t` x) .ih z)))
39	38	2ralbidv 1680	. . . . . . . . 9 |- (v = t -> (A.x e. H~ A.z e. H~ (x .ih (y` z)) = ((v` x) .ih z) <-> A.x e. H~ A.z e. H~ (x .ih (y` z)) = ((t` x) .ih z)))
40	35, 39	3anbi23d 896	. . . . . . . 8 |- (v = t -> ((y:H~-->H~ /\ v:H~-->H~ /\ A.x e. H~ A.z e. H~ (x .ih (y` z)) = ((v` x) .ih z)) <-> (y:H~-->H~ /\ t:H~-->H~ /\ A.x e. H~ A.z e. H~ (x .ih (y` z)) = ((t` x) .ih z))))
41	27, 28, 34, 40	opelopab 2820	. . . . . . 7 |- (<.y, t>. e. {<.u, v>. | (u:H~-->H~ /\ v:H~-->H~ /\ A.x e. H~ A.z e. H~ (x .ih (u` z)) = ((v` x) .ih z))} <-> (y:H~-->H~ /\ t:H~-->H~ /\ A.x e. H~ A.z e. H~ (x .ih (y` z)) = ((t` x) .ih z)))
42	26, 41	bitr2 174	. . . . . 6 |- ((y:H~-->H~ /\ t:H~-->H~ /\ A.x e. H~ A.z e. H~ (x .ih (y` z)) = ((t` x) .ih z)) <-> <.y, t>. e. adjh)
43	24, 42	syl6ib 212	. . . . 5 |- (y e. (LinOp i^i ConOp) -> ((t e. (LinOp i^i ConOp) /\ A.x e. H~ A.z e. H~ ((y` x) .ih z) = (x .ih (t` z))) -> <.y, t>. e. adjh))
44	43	19.22dv 1290	. . . 4 |- (y e. (LinOp i^i ConOp) -> (E.t(t e. (LinOp i^i ConOp) /\ A.x e. H~ A.z e. H~ ((y` x) .ih z) = (x .ih (t` z))) -> E.t<.y, t>. e. adjh))
45	3, 44	mpd 26	. . 3 |- (y e. (LinOp i^i ConOp) -> E.t<.y, t>. e. adjh)
46	27	eldm2 3308	. . 3 |- (y e. dom adjh <-> E.t<.y, t>. e. adj