# Metamath Proof Explorer

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

Ref Expression
Assertion adjmo $⊢ ∃* u u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y$

### Proof

Step Hyp Ref Expression
1 r19.26-2 $⊢ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ∧ x ⋅ ih T ⁡ y = v ⁡ x ⋅ ih y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = v ⁡ x ⋅ ih y$
2 eqtr2 $⊢ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ∧ x ⋅ ih T ⁡ y = v ⁡ x ⋅ ih y → u ⁡ x ⋅ ih y = v ⁡ x ⋅ ih y$
3 2 2ralimi $⊢ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ∧ x ⋅ ih T ⁡ y = v ⁡ x ⋅ ih y → ∀ x ∈ ℋ ∀ y ∈ ℋ u ⁡ x ⋅ ih y = v ⁡ x ⋅ ih y$
4 1 3 sylbir $⊢ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = v ⁡ x ⋅ ih y → ∀ x ∈ ℋ ∀ y ∈ ℋ u ⁡ x ⋅ ih y = v ⁡ x ⋅ ih y$
5 hoeq1 $⊢ u : ℋ ⟶ ℋ ∧ v : ℋ ⟶ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ u ⁡ x ⋅ ih y = v ⁡ x ⋅ ih y ↔ u = v$
6 5 biimpa $⊢ u : ℋ ⟶ ℋ ∧ v : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ u ⁡ x ⋅ ih y = v ⁡ x ⋅ ih y → u = v$
7 4 6 sylan2 $⊢ u : ℋ ⟶ ℋ ∧ v : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = v ⁡ x ⋅ ih y → u = v$
8 7 an4s $⊢ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ∧ v : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = v ⁡ x ⋅ ih y → u = v$
9 8 gen2 $⊢ ∀ u ∀ v u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ∧ v : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = v ⁡ x ⋅ ih y → u = v$
10 feq1 $⊢ u = v → u : ℋ ⟶ ℋ ↔ v : ℋ ⟶ ℋ$
11 fveq1 $⊢ u = v → u ⁡ x = v ⁡ x$
12 11 oveq1d $⊢ u = v → u ⁡ x ⋅ ih y = v ⁡ x ⋅ ih y$
13 12 eqeq2d $⊢ u = v → x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ↔ x ⋅ ih T ⁡ y = v ⁡ x ⋅ ih y$
14 13 2ralbidv $⊢ u = v → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = v ⁡ x ⋅ ih y$
15 10 14 anbi12d $⊢ u = v → u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ↔ v : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = v ⁡ x ⋅ ih y$
16 15 mo4 $⊢ ∃* u u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ↔ ∀ u ∀ v u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ∧ v : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = v ⁡ x ⋅ ih y → u = v$
17 9 16 mpbir $⊢ ∃* u u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y$