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

Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( 𝑇 ∈ 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ℎ ‘ 𝐴 ) )