Theorem unopadj2

Description: The adjoint of a unitary operator is its inverse (converse). Equation 2 of AkhiezerGlazman p. 72. (Contributed by NM, 23-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	unopadj2	⊢ ( 𝑇 ∈ UniOp → ( adjℎ ‘ 𝑇 ) = ◡ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		unoplin	⊢ ( 𝑇 ∈ UniOp → 𝑇 ∈ LinOp )
2		lnopf	⊢ ( 𝑇 ∈ LinOp → 𝑇 : ℋ ⟶ ℋ )
3	1 2	syl	⊢ ( 𝑇 ∈ UniOp → 𝑇 : ℋ ⟶ ℋ )
4		cnvunop	⊢ ( 𝑇 ∈ UniOp → ◡ 𝑇 ∈ UniOp )
5		unoplin	⊢ ( ◡ 𝑇 ∈ UniOp → ◡ 𝑇 ∈ LinOp )
6		lnopf	⊢ ( ◡ 𝑇 ∈ LinOp → ◡ 𝑇 : ℋ ⟶ ℋ )
7	4 5 6	3syl	⊢ ( 𝑇 ∈ UniOp → ◡ 𝑇 : ℋ ⟶ ℋ )
8		unopadj	⊢ ( ( 𝑇 ∈ UniOp ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ◡ 𝑇 ‘ 𝑦 ) ) )
9	8	3expib	⊢ ( 𝑇 ∈ UniOp → ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ◡ 𝑇 ‘ 𝑦 ) ) ) )
10	9	ralrimivv	⊢ ( 𝑇 ∈ UniOp → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ◡ 𝑇 ‘ 𝑦 ) ) )
11		adjeq	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ ◡ 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ◡ 𝑇 ‘ 𝑦 ) ) ) → ( adjℎ ‘ 𝑇 ) = ◡ 𝑇 )
12	3 7 10 11	syl3anc	⊢ ( 𝑇 ∈ UniOp → ( adjℎ ‘ 𝑇 ) = ◡ 𝑇 )