Theorem lnopunii

Description: If a linear operator (whose range is ~H ) is idempotent in the norm, the operator is unitary. Similar to theorem in AkhiezerGlazman p. 73. (Contributed by NM, 23-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lnopuni.1	⊢ 𝑇 ∈ LinOp
	lnopuni.2	⊢ 𝑇 : ℋ –onto→ ℋ
	lnopuni.3	⊢ ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) = ( normℎ ‘ 𝑥 )
Assertion	lnopunii	⊢ 𝑇 ∈ UniOp

Proof

Step	Hyp	Ref	Expression
1		lnopuni.1	⊢ 𝑇 ∈ LinOp
2		lnopuni.2	⊢ 𝑇 : ℋ –onto→ ℋ
3		lnopuni.3	⊢ ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) = ( normℎ ‘ 𝑥 )
4		fveq2	⊢ ( 𝑥 = if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ) )
5	4	oveq1d	⊢ ( 𝑥 = if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ) ·ih ( 𝑇 ‘ 𝑦 ) ) )
6		oveq1	⊢ ( 𝑥 = if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) → ( 𝑥 ·ih 𝑦 ) = ( if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ·ih 𝑦 ) )
7	5 6	eqeq12d	⊢ ( 𝑥 = if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) → ( ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ↔ ( ( 𝑇 ‘ if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ·ih 𝑦 ) ) )
8		fveq2	⊢ ( 𝑦 = if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) → ( 𝑇 ‘ 𝑦 ) = ( 𝑇 ‘ if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ) )
9	8	oveq2d	⊢ ( 𝑦 = if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) → ( ( 𝑇 ‘ if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ) ·ih ( 𝑇 ‘ if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ) ) )
10		oveq2	⊢ ( 𝑦 = if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) → ( if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ·ih 𝑦 ) = ( if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ·ih if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ) )
11	9 10	eqeq12d	⊢ ( 𝑦 = if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) → ( ( ( 𝑇 ‘ if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ·ih 𝑦 ) ↔ ( ( 𝑇 ‘ if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ) ·ih ( 𝑇 ‘ if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ) ) = ( if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ·ih if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ) ) )
12		ifhvhv0	⊢ if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ∈ ℋ
13		ifhvhv0	⊢ if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ∈ ℋ
14	1 3 12 13	lnopunilem2	⊢ ( ( 𝑇 ‘ if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ) ·ih ( 𝑇 ‘ if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ) ) = ( if ( 𝑥 ∈ ℋ , 𝑥 , 0ℎ ) ·ih if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) )
15	7 11 14	dedth2h	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) )
16	15	rgen2	⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 )
17		elunop	⊢ ( 𝑇 ∈ UniOp ↔ ( 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ) )
18	2 16 17	mpbir2an	⊢ 𝑇 ∈ UniOp