# Metamath Proof Explorer

Description: An operator is Hermitian iff it is self-adjoint. Definition of Hermitian in Halmos p. 41. (Contributed by NM, 9-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopadj2 $⊢ T ∈ dom ⁡ adj h → T ∈ HrmOp ↔ adj h ⁡ T = T$

### Proof

Step Hyp Ref Expression
1 hmopadj $⊢ T ∈ HrmOp → adj h ⁡ T = T$
2 dmadjop $⊢ T ∈ dom ⁡ adj h → T : ℋ ⟶ ℋ$
3 2 adantr $⊢ T ∈ dom ⁡ adj h ∧ adj h ⁡ T = T → T : ℋ ⟶ ℋ$
4 adj1 $⊢ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y = adj h ⁡ T ⁡ x ⋅ ih y$
5 4 3expb $⊢ T ∈ dom ⁡ adj h ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y = adj h ⁡ T ⁡ x ⋅ ih y$
6 5 adantlr $⊢ T ∈ dom ⁡ adj h ∧ adj h ⁡ T = T ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y = adj h ⁡ T ⁡ x ⋅ ih y$
7 fveq1 $⊢ adj h ⁡ T = T → adj h ⁡ T ⁡ x = T ⁡ x$
8 7 oveq1d $⊢ adj h ⁡ T = T → adj h ⁡ T ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y$
9 8 ad2antlr $⊢ T ∈ dom ⁡ adj h ∧ adj h ⁡ T = T ∧ x ∈ ℋ ∧ y ∈ ℋ → adj h ⁡ T ⁡ x ⋅ ih y = T ⁡ x ⋅ ih y$
10 6 9 eqtrd $⊢ T ∈ dom ⁡ adj h ∧ adj h ⁡ T = T ∧ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y$
11 10 ralrimivva $⊢ T ∈ dom ⁡ adj h ∧ adj h ⁡ T = T → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y$
12 elhmop $⊢ T ∈ HrmOp ↔ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y$
13 3 11 12 sylanbrc $⊢ T ∈ dom ⁡ adj h ∧ adj h ⁡ T = T → T ∈ HrmOp$
14 13 ex $⊢ T ∈ dom ⁡ adj h → adj h ⁡ T = T → T ∈ HrmOp$
15 1 14 impbid2 $⊢ T ∈ dom ⁡ adj h → T ∈ HrmOp ↔ adj h ⁡ T = T$