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

Metamath Proof Explorer

Theorem idunop

Description: The identity function (restricted to Hilbert space) is a unitary operator. (Contributed by NM, 21-Jan-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	idunop	⊢ ( I ↾ ℋ ) ∈ UniOp

Proof

Step	Hyp	Ref	Expression
1		f1oi	⊢ ( I ↾ ℋ ) : ℋ –1-1-onto→ ℋ
2		f1ofo	⊢ ( ( I ↾ ℋ ) : ℋ –1-1-onto→ ℋ → ( I ↾ ℋ ) : ℋ –onto→ ℋ )
3	1 2	ax-mp	⊢ ( I ↾ ℋ ) : ℋ –onto→ ℋ
4		fvresi	⊢ ( 𝑥 ∈ ℋ → ( ( I ↾ ℋ ) ‘ 𝑥 ) = 𝑥 )
5		fvresi	⊢ ( 𝑦 ∈ ℋ → ( ( I ↾ ℋ ) ‘ 𝑦 ) = 𝑦 )
6	4 5	oveqan12d	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( I ↾ ℋ ) ‘ 𝑥 ) ·_ih ( ( I ↾ ℋ ) ‘ 𝑦 ) ) = ( 𝑥 ·_ih 𝑦 ) )
7	6	rgen2	⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( I ↾ ℋ ) ‘ 𝑥 ) ·_ih ( ( I ↾ ℋ ) ‘ 𝑦 ) ) = ( 𝑥 ·_ih 𝑦 )
8		elunop	⊢ ( ( I ↾ ℋ ) ∈ UniOp ↔ ( ( I ↾ ℋ ) : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( ( I ↾ ℋ ) ‘ 𝑥 ) ·_ih ( ( I ↾ ℋ ) ‘ 𝑦 ) ) = ( 𝑥 ·_ih 𝑦 ) ) )
9	3 7 8	mpbir2an	⊢ ( I ↾ ℋ ) ∈ UniOp