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ℎ

Proof

Step Hyp Ref Expression
1 cnlnadj ⊢ ( 𝑦 ∈ ( LinOp ∩ ContOp ) → ∃ 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) )
2 df-rex ⊢ ( ∃ 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) ↔ ∃ 𝑡 ( 𝑡 ∈ ( LinOp ∩ ContOp ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) ) )
3 1 2 sylib ⊢ ( 𝑦 ∈ ( LinOp ∩ ContOp ) → ∃ 𝑡 ( 𝑡 ∈ ( LinOp ∩ ContOp ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) ) )
4 inss1 ⊢ ( LinOp ∩ ContOp ) ⊆ LinOp
5 4 sseli ⊢ ( 𝑦 ∈ ( LinOp ∩ ContOp ) → 𝑦 ∈ LinOp )
6 lnopf ⊢ ( 𝑦 ∈ LinOp → 𝑦 : ℋ ⟶ ℋ )
7 5 6 syl ⊢ ( 𝑦 ∈ ( LinOp ∩ ContOp ) → 𝑦 : ℋ ⟶ ℋ )
8 7 a1d ⊢ ( 𝑦 ∈ ( LinOp ∩ ContOp ) → ( ( 𝑡 ∈ ( LinOp ∩ ContOp ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) ) → 𝑦 : ℋ ⟶ ℋ ) )
9 4 sseli ⊢ ( 𝑡 ∈ ( LinOp ∩ ContOp ) → 𝑡 ∈ LinOp )
10 lnopf ⊢ ( 𝑡 ∈ LinOp → 𝑡 : ℋ ⟶ ℋ )
11 9 10 syl ⊢ ( 𝑡 ∈ ( LinOp ∩ ContOp ) → 𝑡 : ℋ ⟶ ℋ )
12 11 a1i ⊢ ( 𝑦 ∈ ( LinOp ∩ ContOp ) → ( 𝑡 ∈ ( LinOp ∩ ContOp ) → 𝑡 : ℋ ⟶ ℋ ) )
13 12 adantrd ⊢ ( 𝑦 ∈ ( LinOp ∩ ContOp ) → ( ( 𝑡 ∈ ( LinOp ∩ ContOp ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) ) → 𝑡 : ℋ ⟶ ℋ ) )
14 eqcom ⊢ ( ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) ↔ ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) = ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) )
15 14 biimpi ⊢ ( ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) → ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) = ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) )
16 15 2ralimi ⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) → ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) = ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) )
17 adjsym ⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑦 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) = ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑧 ) ) )
18 11 7 17 syl2anr ⊢ ( ( 𝑦 ∈ ( LinOp ∩ ContOp ) ∧ 𝑡 ∈ ( LinOp ∩ ContOp ) ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) = ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑧 ) ) )
19 16 18 syl5ib ⊢ ( ( 𝑦 ∈ ( LinOp ∩ ContOp ) ∧ 𝑡 ∈ ( LinOp ∩ ContOp ) ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) → ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑧 ) ) )
20 19 expimpd ⊢ ( 𝑦 ∈ ( LinOp ∩ ContOp ) → ( ( 𝑡 ∈ ( LinOp ∩ ContOp ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) ) → ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑧 ) ) )
21 8 13 20 3jcad ⊢ ( 𝑦 ∈ ( LinOp ∩ ContOp ) → ( ( 𝑡 ∈ ( LinOp ∩ ContOp ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) ) → ( 𝑦 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑧 ) ) ) )
22 dfadj2 ⊢ adjℎ = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑣 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑧 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑧 ) ) }
23 22 eleq2i ⊢ ( ⟨ 𝑦 , 𝑡 ⟩ ∈ adjℎ ↔ ⟨ 𝑦 , 𝑡 ⟩ ∈ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑣 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑧 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑧 ) ) } )
24 vex ⊢ 𝑦 ∈ V
25 vex ⊢ 𝑡 ∈ V
26 feq1 ⊢ ( 𝑢 = 𝑦 → ( 𝑢 : ℋ ⟶ ℋ ↔ 𝑦 : ℋ ⟶ ℋ ) )
27 fveq1 ⊢ ( 𝑢 = 𝑦 → ( 𝑢 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) )
28 27 oveq2d ⊢ ( 𝑢 = 𝑦 → ( 𝑥 ·ih ( 𝑢 ‘ 𝑧 ) ) = ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) )
29 28 eqeq1d ⊢ ( 𝑢 = 𝑦 → ( ( 𝑥 ·ih ( 𝑢 ‘ 𝑧 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑧 ) ↔ ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑧 ) ) )
30 29 2ralbidv ⊢ ( 𝑢 = 𝑦 → ( ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑧 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑧 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑧 ) ) )
31 26 30 3anbi13d ⊢ ( 𝑢 = 𝑦 → ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑣 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑧 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑧 ) ) ↔ ( 𝑦 : ℋ ⟶ ℋ ∧ 𝑣 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑧 ) ) ) )
32 feq1 ⊢ ( 𝑣 = 𝑡 → ( 𝑣 : ℋ ⟶ ℋ ↔ 𝑡 : ℋ ⟶ ℋ ) )
33 fveq1 ⊢ ( 𝑣 = 𝑡 → ( 𝑣 ‘ 𝑥 ) = ( 𝑡 ‘ 𝑥 ) )
34 33 oveq1d ⊢ ( 𝑣 = 𝑡 → ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑧 ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑧 ) )
35 34 eqeq2d ⊢ ( 𝑣 = 𝑡 → ( ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑧 ) ↔ ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑧 ) ) )
36 35 2ralbidv ⊢ ( 𝑣 = 𝑡 → ( ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑧 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑧 ) ) )
37 32 36 3anbi23d ⊢ ( 𝑣 = 𝑡 → ( ( 𝑦 : ℋ ⟶ ℋ ∧ 𝑣 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑧 ) ) ↔ ( 𝑦 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑧 ) ) ) )
38 24 25 31 37 opelopab ⊢ ( ⟨ 𝑦 , 𝑡 ⟩ ∈ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑣 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑧 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑧 ) ) } ↔ ( 𝑦 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑧 ) ) )
39 23 38 bitr2i ⊢ ( ( 𝑦 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑥 ·ih ( 𝑦 ‘ 𝑧 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑧 ) ) ↔ ⟨ 𝑦 , 𝑡 ⟩ ∈ adjℎ )
40 21 39 syl6ib ⊢ ( 𝑦 ∈ ( LinOp ∩ ContOp ) → ( ( 𝑡 ∈ ( LinOp ∩ ContOp ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) ) → ⟨ 𝑦 , 𝑡 ⟩ ∈ adjℎ ) )
41 40 eximdv ⊢ ( 𝑦 ∈ ( LinOp ∩ ContOp ) → ( ∃ 𝑡 ( 𝑡 ∈ ( LinOp ∩ ContOp ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑦 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) ) → ∃ 𝑡 ⟨ 𝑦 , 𝑡 ⟩ ∈ adjℎ ) )
42 3 41 mpd ⊢ ( 𝑦 ∈ ( LinOp ∩ ContOp ) → ∃ 𝑡 ⟨ 𝑦 , 𝑡 ⟩ ∈ adjℎ )
43 24 eldm2 ⊢ ( 𝑦 ∈ dom adjℎ ↔ ∃ 𝑡 ⟨ 𝑦 , 𝑡 ⟩ ∈ adjℎ )
44 42 43 sylibr ⊢ ( 𝑦 ∈ ( LinOp ∩ ContOp ) → 𝑦 ∈ dom adjℎ )
45 44 ssriv ⊢ ( LinOp ∩ ContOp ) ⊆ dom adjℎ