Theorem adjmo

Description: Every Hilbert space operator has at most one adjoint. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	adjmo	⊢ ∃* 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		r19.26-2	⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ∧ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) ) )
2		eqtr2	⊢ ( ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ∧ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) ) → ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) )
3	2	2ralimi	⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ∧ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) ) → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) )
4	1 3	sylbir	⊢ ( ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) ) → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) )
5		hoeq1	⊢ ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑣 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) ↔ 𝑢 = 𝑣 ) )
6	5	biimpa	⊢ ( ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑣 : ℋ ⟶ ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) ) → 𝑢 = 𝑣 )
7	4 6	sylan2	⊢ ( ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑣 : ℋ ⟶ ℋ ) ∧ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) ) ) → 𝑢 = 𝑣 )
8	7	an4s	⊢ ( ( ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ∧ ( 𝑣 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) ) ) → 𝑢 = 𝑣 )
9	8	gen2	⊢ ∀ 𝑢 ∀ 𝑣 ( ( ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ∧ ( 𝑣 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) ) ) → 𝑢 = 𝑣 )
10		feq1	⊢ ( 𝑢 = 𝑣 → ( 𝑢 : ℋ ⟶ ℋ ↔ 𝑣 : ℋ ⟶ ℋ ) )
11		fveq1	⊢ ( 𝑢 = 𝑣 → ( 𝑢 ‘ 𝑥 ) = ( 𝑣 ‘ 𝑥 ) )
12	11	oveq1d	⊢ ( 𝑢 = 𝑣 → ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) )
13	12	eqeq2d	⊢ ( 𝑢 = 𝑣 → ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) ) )
14	13	2ralbidv	⊢ ( 𝑢 = 𝑣 → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) ) )
15	10 14	anbi12d	⊢ ( 𝑢 = 𝑣 → ( ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ( 𝑣 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) ) ) )
16	15	mo4	⊢ ( ∃* 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ↔ ∀ 𝑢 ∀ 𝑣 ( ( ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) ∧ ( 𝑣 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑣 ‘ 𝑥 ) ·ih 𝑦 ) ) ) → 𝑢 = 𝑣 ) )
17	9 16	mpbir	⊢ ∃* 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) )