Metamath Proof Explorer

Theorem hmop

Description: Basic inner product property of a Hermitian operator. (Contributed by NM, 19-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion hmop ⊢ T ∈ HrmOp ∧ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih T ⁡ B = T ⁡ A ⋅ ih B

Proof

Step Hyp Ref Expression
1 elhmop ⊢ T ∈ HrmOp ↔ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
2 1 simprbi ⊢ T ∈ HrmOp → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
3 2 3ad2ant1 ⊢ T ∈ HrmOp ∧ A ∈ ℋ ∧ B ∈ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
4 oveq1 ⊢ x = A → x ⋅ ih T ⁡ y = A ⋅ ih T ⁡ y
5 fveq2 ⊢ x = A → T ⁡ x = T ⁡ A
6 5 oveq1d ⊢ x = A → T ⁡ x ⋅ ih y = T ⁡ A ⋅ ih y
7 4 6 eqeq12d ⊢ x = A → x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y ↔ A ⋅ ih T ⁡ y = T ⁡ A ⋅ ih y
8 fveq2 ⊢ y = B → T ⁡ y = T ⁡ B
9 8 oveq2d ⊢ y = B → A ⋅ ih T ⁡ y = A ⋅ ih T ⁡ B
10 oveq2 ⊢ y = B → T ⁡ A ⋅ ih y = T ⁡ A ⋅ ih B
11 9 10 eqeq12d ⊢ y = B → A ⋅ ih T ⁡ y = T ⁡ A ⋅ ih y ↔ A ⋅ ih T ⁡ B = T ⁡ A ⋅ ih B
12 7 11 rspc2v ⊢ A ∈ ℋ ∧ B ∈ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y → A ⋅ ih T ⁡ B = T ⁡ A ⋅ ih B
13 12 3adant1 ⊢ T ∈ HrmOp ∧ A ∈ ℋ ∧ B ∈ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y → A ⋅ ih T ⁡ B = T ⁡ A ⋅ ih B
14 3 13 mpd ⊢ T ∈ HrmOp ∧ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih T ⁡ B = T ⁡ A ⋅ ih B