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 ffvelcdmda ⊢ 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