This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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_ℎ ‘ 𝑇 ) = ^◡ 𝑇 )