Metamath Proof Explorer

Theorem hmopadj2

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