Theorem unopnorm

Description: A unitary operator is idempotent in the norm. (Contributed by NM, 25-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	unopnorm	⊢ ( ( 𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) = ( normℎ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		unopf1o	⊢ ( 𝑇 ∈ UniOp → 𝑇 : ℋ –1-1-onto→ ℋ )
2		f1of	⊢ ( 𝑇 : ℋ –1-1-onto→ ℋ → 𝑇 : ℋ ⟶ ℋ )
3	1 2	syl	⊢ ( 𝑇 ∈ UniOp → 𝑇 : ℋ ⟶ ℋ )
4	3	ffvelrnda	⊢ ( ( 𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ) → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
5		normcl	⊢ ( ( 𝑇 ‘ 𝐴 ) ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ )
6	4 5	syl	⊢ ( ( 𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ )
7		normcl	⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ 𝐴 ) ∈ ℝ )
8	7	adantl	⊢ ( ( 𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ) → ( normℎ ‘ 𝐴 ) ∈ ℝ )
9		normge0	⊢ ( ( 𝑇 ‘ 𝐴 ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) )
10	4 9	syl	⊢ ( ( 𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ) → 0 ≤ ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) )
11		normge0	⊢ ( 𝐴 ∈ ℋ → 0 ≤ ( normℎ ‘ 𝐴 ) )
12	11	adantl	⊢ ( ( 𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ) → 0 ≤ ( normℎ ‘ 𝐴 ) )
13		unop	⊢ ( ( 𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) = ( 𝐴 ·ih 𝐴 ) )
14	13	3anidm23	⊢ ( ( 𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) = ( 𝐴 ·ih 𝐴 ) )
15		normsq	⊢ ( ( 𝑇 ‘ 𝐴 ) ∈ ℋ → ( ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ↑ 2 ) = ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) )
16	4 15	syl	⊢ ( ( 𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ↑ 2 ) = ( ( 𝑇 ‘ 𝐴 ) ·ih ( 𝑇 ‘ 𝐴 ) ) )
17		normsq	⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 ·ih 𝐴 ) )
18	17	adantl	⊢ ( ( 𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ) → ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 ·ih 𝐴 ) )
19	14 16 18	3eqtr4d	⊢ ( ( 𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ↑ 2 ) = ( ( normℎ ‘ 𝐴 ) ↑ 2 ) )
20	6 8 10 12 19	sq11d	⊢ ( ( 𝑇 ∈ UniOp ∧ 𝐴 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) = ( normℎ ‘ 𝐴 ) )