Metamath Proof Explorer

Theorem dfadj2

Description: Alternate definition of the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion dfadj2 ⊢ adj h = t u | t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y

Proof

Step Hyp Ref Expression
1 df-adjh ⊢ adj h = t u | t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y
2 eqcom ⊢ t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y ↔ x ⋅ ih u ⁡ y = t ⁡ x ⋅ ih y
3 2 2ralbii ⊢ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih u ⁡ y = t ⁡ x ⋅ ih y
4 adjsym ⊢ t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih u ⁡ y = t ⁡ x ⋅ ih y
5 3 4 bitr4id ⊢ t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
6 5 pm5.32i ⊢ t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y ↔ t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
7 df-3an ⊢ t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y ↔ t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y
8 df-3an ⊢ t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y ↔ t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
9 6 7 8 3bitr4i ⊢ t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y ↔ t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
10 9 opabbii ⊢ t u | t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ t ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y = t u | t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y
11 1 10 eqtri ⊢ adj h = t u | t : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = u ⁡ x ⋅ ih y