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

Metamath Proof Explorer

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 𝑦 ) )