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 ( 𝑡 ‘ 𝑦 ) )