This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnlnadjeui

Description: Every continuous linear operator has a unique adjoint. Theorem 3.10 of Beran p. 104. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses cnlnadj.1 ⊢ 𝑇 ∈ LinOp
cnlnadj.2 ⊢ 𝑇 ∈ ContOp
Assertion cnlnadjeui ∃! 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 cnlnadj.1 ⊢ 𝑇 ∈ LinOp
2 cnlnadj.2 ⊢ 𝑇 ∈ ContOp
3 1 2 cnlnadji ⊢ ∃ 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) )
4 adjmo ⊢ ∃* 𝑡 ( 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) )
5 inss1 ⊢ ( LinOp ∩ ContOp ) ⊆ LinOp
6 5 sseli ⊢ ( 𝑡 ∈ ( LinOp ∩ ContOp ) → 𝑡 ∈ LinOp )
7 lnopf ⊢ ( 𝑡 ∈ LinOp → 𝑡 : ℋ ⟶ ℋ )
8 6 7 syl ⊢ ( 𝑡 ∈ ( LinOp ∩ ContOp ) → 𝑡 : ℋ ⟶ ℋ )
9 simpl ⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ) → 𝑡 : ℋ ⟶ ℋ )
10 eqcom ⊢ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ↔ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) )
11 10 2ralbii ⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) )
12 1 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
13 adjsym ⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) )
14 12 13 mpan2 ⊢ ( 𝑡 : ℋ ⟶ ℋ → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) )
15 11 14 bitrid ⊢ ( 𝑡 : ℋ ⟶ ℋ → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) )
16 15 biimpa ⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) )
17 9 16 jca ⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ) → ( 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) )
18 8 17 sylan ⊢ ( ( 𝑡 ∈ ( LinOp ∩ ContOp ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ) → ( 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) )
19 18 moimi ⊢ ( ∃* 𝑡 ( 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) → ∃* 𝑡 ( 𝑡 ∈ ( LinOp ∩ ContOp ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ) )
20 df-rmo ⊢ ( ∃* 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ↔ ∃* 𝑡 ( 𝑡 ∈ ( LinOp ∩ ContOp ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ) )
21 19 20 sylibr ⊢ ( ∃* 𝑡 ( 𝑡 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) → ∃* 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) )
22 4 21 ax-mp ⊢ ∃* 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) )
23 reu5 ⊢ ( ∃! 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ↔ ( ∃ 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ∧ ∃* 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ) )
24 3 22 23 mpbir2an ⊢ ∃! 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) )