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

Metamath Proof Explorer

Theorem cnlnadjeu

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

Ref Expression
Assertion cnlnadjeu ( 𝑇 ∈ ( LinOp ∩ ContOp ) → ∃! 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0hop ) → ( 𝑇 ‘ 𝑥 ) = ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0hop ) ‘ 𝑥 ) )
2 1 oveq1d ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0hop ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑦 ) )
3 2 eqeq1d ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0hop ) → ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ↔ ( ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ) )
4 3 2ralbidv ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0hop ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ) )
5 4 reubidv ⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0hop ) → ( ∃! 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ↔ ∃! 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ) )
6 inss1 ⊢ ( LinOp ∩ ContOp ) ⊆ LinOp
7 0lnop ⊢ 0hop ∈ LinOp
8 0cnop ⊢ 0hop ∈ ContOp
9 elin ⊢ ( 0hop ∈ ( LinOp ∩ ContOp ) ↔ ( 0hop ∈ LinOp ∧ 0hop ∈ ContOp ) )
10 7 8 9 mpbir2an ⊢ 0hop ∈ ( LinOp ∩ ContOp )
11 10 elimel ⊢ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0hop ) ∈ ( LinOp ∩ ContOp )
12 6 11 sselii ⊢ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0hop ) ∈ LinOp
13 inss2 ⊢ ( LinOp ∩ ContOp ) ⊆ ContOp
14 13 11 sselii ⊢ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0hop ) ∈ ContOp
15 12 14 cnlnadjeui ⊢ ∃! 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) )
16 5 15 dedth ⊢ ( 𝑇 ∈ ( LinOp ∩ ContOp ) → ∃! 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) )