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 e. UniOp /\ A e. ~H ) -> ( normh ` ( T ` A ) ) = ( normh ` A ) )

Proof

Step Hyp Ref Expression
1 unopf1o 
 |-  ( T e. UniOp -> T : ~H -1-1-onto-> ~H )
2 f1of 
 |-  ( T : ~H -1-1-onto-> ~H -> T : ~H --> ~H )
3 1 2 syl 
 |-  ( T e. UniOp -> T : ~H --> ~H )
4 3 ffvelrnda 
 |-  ( ( T e. UniOp /\ A e. ~H ) -> ( T ` A ) e. ~H )
5 normcl 
 |-  ( ( T ` A ) e. ~H -> ( normh ` ( T ` A ) ) e. RR )
6 4 5 syl 
 |-  ( ( T e. UniOp /\ A e. ~H ) -> ( normh ` ( T ` A ) ) e. RR )
7 normcl 
 |-  ( A e. ~H -> ( normh ` A ) e. RR )
8 7 adantl 
 |-  ( ( T e. UniOp /\ A e. ~H ) -> ( normh ` A ) e. RR )
9 normge0 
 |-  ( ( T ` A ) e. ~H -> 0 <_ ( normh ` ( T ` A ) ) )
10 4 9 syl 
 |-  ( ( T e. UniOp /\ A e. ~H ) -> 0 <_ ( normh ` ( T ` A ) ) )
11 normge0 
 |-  ( A e. ~H -> 0 <_ ( normh ` A ) )
12 11 adantl 
 |-  ( ( T e. UniOp /\ A e. ~H ) -> 0 <_ ( normh ` A ) )
13 unop 
 |-  ( ( T e. UniOp /\ A e. ~H /\ A e. ~H ) -> ( ( T ` A ) .ih ( T ` A ) ) = ( A .ih A ) )
14 13 3anidm23 
 |-  ( ( T e. UniOp /\ A e. ~H ) -> ( ( T ` A ) .ih ( T ` A ) ) = ( A .ih A ) )
15 normsq 
 |-  ( ( T ` A ) e. ~H -> ( ( normh ` ( T ` A ) ) ^ 2 ) = ( ( T ` A ) .ih ( T ` A ) ) )
16 4 15 syl 
 |-  ( ( T e. UniOp /\ A e. ~H ) -> ( ( normh ` ( T ` A ) ) ^ 2 ) = ( ( T ` A ) .ih ( T ` A ) ) )
17 normsq 
 |-  ( A e. ~H -> ( ( normh ` A ) ^ 2 ) = ( A .ih A ) )
18 17 adantl 
 |-  ( ( T e. UniOp /\ A e. ~H ) -> ( ( normh ` A ) ^ 2 ) = ( A .ih A ) )
19 14 16 18 3eqtr4d 
 |-  ( ( T e. UniOp /\ A e. ~H ) -> ( ( normh ` ( T ` A ) ) ^ 2 ) = ( ( normh ` A ) ^ 2 ) )
20 6 8 10 12 19 sq11d 
 |-  ( ( T e. UniOp /\ A e. ~H ) -> ( normh ` ( T ` A ) ) = ( normh ` A ) )