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	⊢ ( 𝑇 ∈ dom adjℎ → ( 𝑇 ∈ HrmOp ↔ ( adjℎ ‘ 𝑇 ) = 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		hmopadj	⊢ ( 𝑇 ∈ HrmOp → ( adjℎ ‘ 𝑇 ) = 𝑇 )
2		dmadjop	⊢ ( 𝑇 ∈ dom adjℎ → 𝑇 : ℋ ⟶ ℋ )
3	2	adantr	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( adjℎ ‘ 𝑇 ) = 𝑇 ) → 𝑇 : ℋ ⟶ ℋ )
4		adj1	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) )
5	4	3expb	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) )
6	5	adantlr	⊢ ( ( ( 𝑇 ∈ dom adjℎ ∧ ( adjℎ ‘ 𝑇 ) = 𝑇 ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) )
7		fveq1	⊢ ( ( adjℎ ‘ 𝑇 ) = 𝑇 → ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
8	7	oveq1d	⊢ ( ( adjℎ ‘ 𝑇 ) = 𝑇 → ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) )
9	8	ad2antlr	⊢ ( ( ( 𝑇 ∈ dom adjℎ ∧ ( adjℎ ‘ 𝑇 ) = 𝑇 ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) )
10	6 9	eqtrd	⊢ ( ( ( 𝑇 ∈ dom adjℎ ∧ ( adjℎ ‘ 𝑇 ) = 𝑇 ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) )
11	10	ralrimivva	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( adjℎ ‘ 𝑇 ) = 𝑇 ) → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) )
12		elhmop	⊢ ( 𝑇 ∈ HrmOp ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ) )
13	3 11 12	sylanbrc	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ ( adjℎ ‘ 𝑇 ) = 𝑇 ) → 𝑇 ∈ HrmOp )
14	13	ex	⊢ ( 𝑇 ∈ dom adjℎ → ( ( adjℎ ‘ 𝑇 ) = 𝑇 → 𝑇 ∈ HrmOp ) )
15	1 14	impbid2	⊢ ( 𝑇 ∈ dom adjℎ → ( 𝑇 ∈ HrmOp ↔ ( adjℎ ‘ 𝑇 ) = 𝑇 ) )