# 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 $⊢ T ∈ UniOp ∧ A ∈ ℋ → norm ℎ ⁡ T ⁡ A = norm ℎ ⁡ A$

### Proof

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