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

Metamath Proof Explorer

Theorem normsubi

Description: Negative doesn't change the norm of a Hilbert space vector. (Contributed by NM, 11-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses normsub.1 
|- A e. ~H
normsub.2 
|- B e. ~H
Assertion normsubi 
|- ( normh ` ( A -h B ) ) = ( normh ` ( B -h A ) )

Proof

Step Hyp Ref Expression
1 normsub.1 
 |-  A e. ~H
2 normsub.2 
 |-  B e. ~H
3 neg1cn 
 |-  -u 1 e. CC
4 2 1 hvsubcli 
 |-  ( B -h A ) e. ~H
5 3 4 norm-iii-i 
 |-  ( normh ` ( -u 1 .h ( B -h A ) ) ) = ( ( abs ` -u 1 ) x. ( normh ` ( B -h A ) ) )
6 2 1 hvnegdii 
 |-  ( -u 1 .h ( B -h A ) ) = ( A -h B )
7 6 fveq2i 
 |-  ( normh ` ( -u 1 .h ( B -h A ) ) ) = ( normh ` ( A -h B ) )
8 ax-1cn 
 |-  1 e. CC
9 8 absnegi 
 |-  ( abs ` -u 1 ) = ( abs ` 1 )
10 abs1 
 |-  ( abs ` 1 ) = 1
11 9 10 eqtri 
 |-  ( abs ` -u 1 ) = 1
12 11 oveq1i 
 |-  ( ( abs ` -u 1 ) x. ( normh ` ( B -h A ) ) ) = ( 1 x. ( normh ` ( B -h A ) ) )
13 4 normcli 
 |-  ( normh ` ( B -h A ) ) e. RR
14 13 recni 
 |-  ( normh ` ( B -h A ) ) e. CC
15 14 mullidi 
 |-  ( 1 x. ( normh ` ( B -h A ) ) ) = ( normh ` ( B -h A ) )
16 12 15 eqtri 
 |-  ( ( abs ` -u 1 ) x. ( normh ` ( B -h A ) ) ) = ( normh ` ( B -h A ) )
17 5 7 16 3eqtr3i 
 |-  ( normh ` ( A -h B ) ) = ( normh ` ( B -h A ) )