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 ⁡ adj h

Proof

Step Hyp Ref Expression
1 cnlnadj ⊢ y ∈ LinOp ∩ ContOp → ∃ t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ z ∈ ℋ y ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z
2 df-rex ⊢ ∃ t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ z ∈ ℋ y ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z ↔ ∃ t t ∈ LinOp ∩ ContOp ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ y ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z
3 1 2 sylib ⊢ y ∈ LinOp ∩ ContOp → ∃ t t ∈ LinOp ∩ ContOp ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ y ⁡ x ⋅ ih z = x ⋅ ih t ⁡ 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 ⋅ ih z = x ⋅ ih t ⁡ 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 ⋅ ih z = x ⋅ ih t ⁡ z → t : ℋ ⟶ ℋ
14 eqcom ⊢ y ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z ↔ x ⋅ ih t ⁡ z = y ⁡ x ⋅ ih z
15 14 biimpi ⊢ y ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z → x ⋅ ih t ⁡ z = y ⁡ x ⋅ ih z
16 15 2ralimi ⊢ ∀ x ∈ ℋ ∀ z ∈ ℋ y ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z → ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih t ⁡ z = y ⁡ x ⋅ ih z
17 adjsym ⊢ t : ℋ ⟶ ℋ ∧ y : ℋ ⟶ ℋ → ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih t ⁡ z = y ⁡ x ⋅ ih z ↔ ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih y ⁡ z = t ⁡ x ⋅ ih z
18 11 7 17 syl2anr ⊢ y ∈ LinOp ∩ ContOp ∧ t ∈ LinOp ∩ ContOp → ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih t ⁡ z = y ⁡ x ⋅ ih z ↔ ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih y ⁡ z = t ⁡ x ⋅ ih z
19 16 18 imbitrid ⊢ y ∈ LinOp ∩ ContOp ∧ t ∈ LinOp ∩ ContOp → ∀ x ∈ ℋ ∀ z ∈ ℋ y ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z → ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih y ⁡ z = t ⁡ x ⋅ ih z
20 19 expimpd ⊢ y ∈ LinOp ∩ ContOp → t ∈ LinOp ∩ ContOp ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ y ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z → ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih y ⁡ z = t ⁡ x ⋅ ih z
21 8 13 20 3jcad ⊢ y ∈ LinOp ∩ ContOp → t ∈ LinOp ∩ ContOp ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ y ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z → y : ℋ ⟶ ℋ ∧ t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih y ⁡ z = t ⁡ x ⋅ ih z
22 dfadj2 ⊢ adj h = u v | u : ℋ ⟶ ℋ ∧ v : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih u ⁡ z = v ⁡ x ⋅ ih z
23 22 eleq2i ⊢ y t ∈ adj h ↔ y t ∈ u v | u : ℋ ⟶ ℋ ∧ v : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih u ⁡ z = v ⁡ x ⋅ ih z
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 ⋅ ih u ⁡ z = x ⋅ ih y ⁡ z
29 28 eqeq1d ⊢ u = y → x ⋅ ih u ⁡ z = v ⁡ x ⋅ ih z ↔ x ⋅ ih y ⁡ z = v ⁡ x ⋅ ih z
30 29 2ralbidv ⊢ u = y → ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih u ⁡ z = v ⁡ x ⋅ ih z ↔ ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih y ⁡ z = v ⁡ x ⋅ ih z
31 26 30 3anbi13d ⊢ u = y → u : ℋ ⟶ ℋ ∧ v : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih u ⁡ z = v ⁡ x ⋅ ih z ↔ y : ℋ ⟶ ℋ ∧ v : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih y ⁡ z = v ⁡ x ⋅ ih z
32 feq1 ⊢ v = t → v : ℋ ⟶ ℋ ↔ t : ℋ ⟶ ℋ
33 fveq1 ⊢ v = t → v ⁡ x = t ⁡ x
34 33 oveq1d ⊢ v = t → v ⁡ x ⋅ ih z = t ⁡ x ⋅ ih z
35 34 eqeq2d ⊢ v = t → x ⋅ ih y ⁡ z = v ⁡ x ⋅ ih z ↔ x ⋅ ih y ⁡ z = t ⁡ x ⋅ ih z
36 35 2ralbidv ⊢ v = t → ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih y ⁡ z = v ⁡ x ⋅ ih z ↔ ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih y ⁡ z = t ⁡ x ⋅ ih z
37 32 36 3anbi23d ⊢ v = t → y : ℋ ⟶ ℋ ∧ v : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih y ⁡ z = v ⁡ x ⋅ ih z ↔ y : ℋ ⟶ ℋ ∧ t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih y ⁡ z = t ⁡ x ⋅ ih z
38 24 25 31 37 opelopab ⊢ y t ∈ u v | u : ℋ ⟶ ℋ ∧ v : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih u ⁡ z = v ⁡ x ⋅ ih z ↔ y : ℋ ⟶ ℋ ∧ t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih y ⁡ z = t ⁡ x ⋅ ih z
39 23 38 bitr2i ⊢ y : ℋ ⟶ ℋ ∧ t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ x ⋅ ih y ⁡ z = t ⁡ x ⋅ ih z ↔ y t ∈ adj h
40 21 39 imbitrdi ⊢ y ∈ LinOp ∩ ContOp → t ∈ LinOp ∩ ContOp ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ y ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z → y t ∈ adj h
41 40 eximdv ⊢ y ∈ LinOp ∩ ContOp → ∃ t t ∈ LinOp ∩ ContOp ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ y ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z → ∃ t y t ∈ adj h
42 3 41 mpd ⊢ y ∈ LinOp ∩ ContOp → ∃ t y t ∈ adj h
43 24 eldm2 ⊢ y ∈ dom ⁡ adj h ↔ ∃ t y t ∈ adj h
44 42 43 sylibr ⊢ y ∈ LinOp ∩ ContOp → y ∈ dom ⁡ adj h
45 44 ssriv ⊢ LinOp ∩ ContOp ⊆ dom ⁡ adj h