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 ⊢ ∃* 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