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 ⊢∃*uu:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihT⁡y=u⁡x⋅ihy

Proof

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