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 ) , 𝑇 , 0_hop ) → ( 𝑇 ‘ 𝑥 ) = ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0_hop ) ‘ 𝑥 ) )
2	1	oveq1d	⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0_hop ) → ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) = ( ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0_hop ) ‘ 𝑥 ) ·_ih 𝑦 ) )
3	2	eqeq1d	⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0_hop ) → ( ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) = ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) ↔ ( ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0_hop ) ‘ 𝑥 ) ·_ih 𝑦 ) = ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) ) )
4	3	2ralbidv	⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0_hop ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) = ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0_hop ) ‘ 𝑥 ) ·_ih 𝑦 ) = ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) ) )
5	4	reubidv	⊢ ( 𝑇 = if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0_hop ) → ( ∃! 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) = ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) ↔ ∃! 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0_hop ) ‘ 𝑥 ) ·_ih 𝑦 ) = ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) ) )
6		inss1	⊢ ( LinOp ∩ ContOp ) ⊆ LinOp
7		0lnop	⊢ 0_hop ∈ LinOp
8		0cnop	⊢ 0_hop ∈ ContOp
9		elin	⊢ ( 0_hop ∈ ( LinOp ∩ ContOp ) ↔ ( 0_hop ∈ LinOp ∧ 0_hop ∈ ContOp ) )
10	7 8 9	mpbir2an	⊢ 0_hop ∈ ( LinOp ∩ ContOp )
11	10	elimel	⊢ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0_hop ) ∈ ( LinOp ∩ ContOp )
12	6 11	sselii	⊢ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0_hop ) ∈ LinOp
13		inss2	⊢ ( LinOp ∩ ContOp ) ⊆ ContOp
14	13 11	sselii	⊢ if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0_hop ) ∈ ContOp
15	12 14	cnlnadjeui	⊢ ∃! 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( if ( 𝑇 ∈ ( LinOp ∩ ContOp ) , 𝑇 , 0_hop ) ‘ 𝑥 ) ·_ih 𝑦 ) = ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) )
16	5 15	dedth	⊢ ( 𝑇 ∈ ( LinOp ∩ ContOp ) → ∃! 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) = ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) )