Metamath Proof Explorer

Theorem cnlnssadj

Description: Every continuous linear Hilbert space operator has an adjoint. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion cnlnssadj ⊢LinOp∩ContOp⊆dom⁡adjh

Proof

Step Hyp Ref Expression
1 cnlnadj ⊢y∈LinOp∩ContOp→∃t∈LinOp∩ContOp∀x∈ℋ∀z∈ℋy⁡x⋅ihz=x⋅iht⁡z
2 df-rex ⊢∃t∈LinOp∩ContOp∀x∈ℋ∀z∈ℋy⁡x⋅ihz=x⋅iht⁡z↔∃tt∈LinOp∩ContOp∧∀x∈ℋ∀z∈ℋy⁡x⋅ihz=x⋅iht⁡z
3 1 2 sylib ⊢y∈LinOp∩ContOp→∃tt∈LinOp∩ContOp∧∀x∈ℋ∀z∈ℋy⁡x⋅ihz=x⋅iht⁡z
4 inss1 ⊢LinOp∩ContOp⊆LinOp
5 4 sseli ⊢y∈LinOp∩ContOp→y∈LinOp
6 lnopf ⊢y∈LinOp→y:ℋ⟶ℋ
7 5 6 syl ⊢y∈LinOp∩ContOp→y:ℋ⟶ℋ
8 7 a1d ⊢y∈LinOp∩ContOp→t∈LinOp∩ContOp∧∀x∈ℋ∀z∈ℋy⁡x⋅ihz=x⋅iht⁡z→y:ℋ⟶ℋ
9 4 sseli ⊢t∈LinOp∩ContOp→t∈LinOp
10 lnopf ⊢t∈LinOp→t:ℋ⟶ℋ
11 9 10 syl ⊢t∈LinOp∩ContOp→t:ℋ⟶ℋ
12 11 a1i ⊢y∈LinOp∩ContOp→t∈LinOp∩ContOp→t:ℋ⟶ℋ
13 12 adantrd ⊢y∈LinOp∩ContOp→t∈LinOp∩ContOp∧∀x∈ℋ∀z∈ℋy⁡x⋅ihz=x⋅iht⁡z→t:ℋ⟶ℋ
14 eqcom ⊢y⁡x⋅ihz=x⋅iht⁡z↔x⋅iht⁡z=y⁡x⋅ihz
15 14 biimpi ⊢y⁡x⋅ihz=x⋅iht⁡z→x⋅iht⁡z=y⁡x⋅ihz
16 15 2ralimi ⊢∀x∈ℋ∀z∈ℋy⁡x⋅ihz=x⋅iht⁡z→∀x∈ℋ∀z∈ℋx⋅iht⁡z=y⁡x⋅ihz
17 adjsym ⊢t:ℋ⟶ℋ∧y:ℋ⟶ℋ→∀x∈ℋ∀z∈ℋx⋅iht⁡z=y⁡x⋅ihz↔∀x∈ℋ∀z∈ℋx⋅ihy⁡z=t⁡x⋅ihz
18 11 7 17 syl2anr ⊢y∈LinOp∩ContOp∧t∈LinOp∩ContOp→∀x∈ℋ∀z∈ℋx⋅iht⁡z=y⁡x⋅ihz↔∀x∈ℋ∀z∈ℋx⋅ihy⁡z=t⁡x⋅ihz
19 16 18 imbitrid ⊢y∈LinOp∩ContOp∧t∈LinOp∩ContOp→∀x∈ℋ∀z∈ℋy⁡x⋅ihz=x⋅iht⁡z→∀x∈ℋ∀z∈ℋx⋅ihy⁡z=t⁡x⋅ihz
20 19 expimpd ⊢y∈LinOp∩ContOp→t∈LinOp∩ContOp∧∀x∈ℋ∀z∈ℋy⁡x⋅ihz=x⋅iht⁡z→∀x∈ℋ∀z∈ℋx⋅ihy⁡z=t⁡x⋅ihz
21 8 13 20 3jcad ⊢y∈LinOp∩ContOp→t∈LinOp∩ContOp∧∀x∈ℋ∀z∈ℋy⁡x⋅ihz=x⋅iht⁡z→y:ℋ⟶ℋ∧t:ℋ⟶ℋ∧∀x∈ℋ∀z∈ℋx⋅ihy⁡z=t⁡x⋅ihz
22 dfadj2 ⊢adjh=uv|u:ℋ⟶ℋ∧v:ℋ⟶ℋ∧∀x∈ℋ∀z∈ℋx⋅ihu⁡z=v⁡x⋅ihz
23 22 eleq2i ⊢yt∈adjh↔yt∈uv|u:ℋ⟶ℋ∧v:ℋ⟶ℋ∧∀x∈ℋ∀z∈ℋx⋅ihu⁡z=v⁡x⋅ihz
24 vex ⊢y∈V
25 vex ⊢t∈V
26 feq1 ⊢u=y→u:ℋ⟶ℋ↔y:ℋ⟶ℋ
27 fveq1 ⊢u=y→u⁡z=y⁡z
28 27 oveq2d ⊢u=y→x⋅ihu⁡z=x⋅ihy⁡z
29 28 eqeq1d ⊢u=y→x⋅ihu⁡z=v⁡x⋅ihz↔x⋅ihy⁡z=v⁡x⋅ihz
30 29 2ralbidv ⊢u=y→∀x∈ℋ∀z∈ℋx⋅ihu⁡z=v⁡x⋅ihz↔∀x∈ℋ∀z∈ℋx⋅ihy⁡z=v⁡x⋅ihz
31 26 30 3anbi13d ⊢u=y→u:ℋ⟶ℋ∧v:ℋ⟶ℋ∧∀x∈ℋ∀z∈ℋx⋅ihu⁡z=v⁡x⋅ihz↔y:ℋ⟶ℋ∧v:ℋ⟶ℋ∧∀x∈ℋ∀z∈ℋx⋅ihy⁡z=v⁡x⋅ihz
32 feq1 ⊢v=t→v:ℋ⟶ℋ↔t:ℋ⟶ℋ
33 fveq1 ⊢v=t→v⁡x=t⁡x
34 33 oveq1d ⊢v=t→v⁡x⋅ihz=t⁡x⋅ihz
35 34 eqeq2d ⊢v=t→x⋅ihy⁡z=v⁡x⋅ihz↔x⋅ihy⁡z=t⁡x⋅ihz
36 35 2ralbidv ⊢v=t→∀x∈ℋ∀z∈ℋx⋅ihy⁡z=v⁡x⋅ihz↔∀x∈ℋ∀z∈ℋx⋅ihy⁡z=t⁡x⋅ihz
37 32 36 3anbi23d ⊢v=t→y:ℋ⟶ℋ∧v:ℋ⟶ℋ∧∀x∈ℋ∀z∈ℋx⋅ihy⁡z=v⁡x⋅ihz↔y:ℋ⟶ℋ∧t:ℋ⟶ℋ∧∀x∈ℋ∀z∈ℋx⋅ihy⁡z=t⁡x⋅ihz
38 24 25 31 37 opelopab ⊢yt∈uv|u:ℋ⟶ℋ∧v:ℋ⟶ℋ∧∀x∈ℋ∀z∈ℋx⋅ihu⁡z=v⁡x⋅ihz↔y:ℋ⟶ℋ∧t:ℋ⟶ℋ∧∀x∈ℋ∀z∈ℋx⋅ihy⁡z=t⁡x⋅ihz
39 23 38 bitr2i ⊢y:ℋ⟶ℋ∧t:ℋ⟶ℋ∧∀x∈ℋ∀z∈ℋx⋅ihy⁡z=t⁡x⋅ihz↔yt∈adjh
40 21 39 imbitrdi ⊢y∈LinOp∩ContOp→t∈LinOp∩ContOp∧∀x∈ℋ∀z∈ℋy⁡x⋅ihz=x⋅iht⁡z→yt∈adjh
41 40 eximdv ⊢y∈LinOp∩ContOp→∃tt∈LinOp∩ContOp∧∀x∈ℋ∀z∈ℋy⁡x⋅ihz=x⋅iht⁡z→∃tyt∈adjh
42 3 41 mpd ⊢y∈LinOp∩ContOp→∃tyt∈adjh
43 24 eldm2 ⊢y∈dom⁡adjh↔∃tyt∈adjh
44 42 43 sylibr ⊢y∈LinOp∩ContOp→y∈dom⁡adjh
45 44 ssriv ⊢LinOp∩ContOp⊆dom⁡adjh