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⋅ihT⁡A=A⋅ihA
14 13 3anidm23 ⊢T∈UniOp∧A∈ℋ→T⁡A⋅ihT⁡A=A⋅ihA
15 normsq ⊢T⁡A∈ℋ→normℎ⁡T⁡A2=T⁡A⋅ihT⁡A
16 4 15 syl ⊢T∈UniOp∧A∈ℋ→normℎ⁡T⁡A2=T⁡A⋅ihT⁡A
17 normsq ⊢A∈ℋ→normℎ⁡A2=A⋅ihA
18 17 adantl ⊢T∈UniOp∧A∈ℋ→normℎ⁡A2=A⋅ihA
19 14 16 18 3eqtr4d ⊢T∈UniOp∧A∈ℋ→normℎ⁡T⁡A2=normℎ⁡A2
20 6 8 10 12 19 sq11d ⊢T∈UniOp∧A∈ℋ→normℎ⁡T⁡A=normℎ⁡A