Metamath Proof Explorer

Theorem nvs

Description: Proportionality property of the norm of a scalar product in a normed complex vector space. (Contributed by NM, 11-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nvs.1 
|- X = ( BaseSet ` U )
nvs.4 
|- S = ( .sOLD ` U )
nvs.6 
|- N = ( normCV ` U )
Assertion nvs 
|- ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( N ` ( A S B ) ) = ( ( abs ` A ) x. ( N ` B ) ) )

Proof

Step Hyp Ref Expression
1 nvs.1 
 |-  X = ( BaseSet ` U )
2 nvs.4 
 |-  S = ( .sOLD ` U )
3 nvs.6 
 |-  N = ( normCV ` U )
4 eqid 
 |-  ( +v ` U ) = ( +v ` U )
5 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
6 1 4 2 5 3 nvi 
 |-  ( U e. NrmCVec -> ( <. ( +v ` U ) , S >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = ( 0vec ` U ) ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x ( +v ` U ) y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )
7 6 simp3d 
 |-  ( U e. NrmCVec -> A. x e. X ( ( ( N ` x ) = 0 -> x = ( 0vec ` U ) ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x ( +v ` U ) y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) )
8 simp2 
 |-  ( ( ( ( N ` x ) = 0 -> x = ( 0vec ` U ) ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x ( +v ` U ) y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) )
9 8 ralimi 
 |-  ( A. x e. X ( ( ( N ` x ) = 0 -> x = ( 0vec ` U ) ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x ( +v ` U ) y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> A. x e. X A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) )
10 7 9 syl 
 |-  ( U e. NrmCVec -> A. x e. X A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) )
11 oveq2 
 |-  ( x = B -> ( y S x ) = ( y S B ) )
12 11 fveq2d 
 |-  ( x = B -> ( N ` ( y S x ) ) = ( N ` ( y S B ) ) )
13 fveq2 
 |-  ( x = B -> ( N ` x ) = ( N ` B ) )
14 13 oveq2d 
 |-  ( x = B -> ( ( abs ` y ) x. ( N ` x ) ) = ( ( abs ` y ) x. ( N ` B ) ) )
15 12 14 eqeq12d 
 |-  ( x = B -> ( ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) <-> ( N ` ( y S B ) ) = ( ( abs ` y ) x. ( N ` B ) ) ) )
16 fvoveq1 
 |-  ( y = A -> ( N ` ( y S B ) ) = ( N ` ( A S B ) ) )
17 fveq2 
 |-  ( y = A -> ( abs ` y ) = ( abs ` A ) )
18 17 oveq1d 
 |-  ( y = A -> ( ( abs ` y ) x. ( N ` B ) ) = ( ( abs ` A ) x. ( N ` B ) ) )
19 16 18 eqeq12d 
 |-  ( y = A -> ( ( N ` ( y S B ) ) = ( ( abs ` y ) x. ( N ` B ) ) <-> ( N ` ( A S B ) ) = ( ( abs ` A ) x. ( N ` B ) ) ) )
20 15 19 rspc2v 
 |-  ( ( B e. X /\ A e. CC ) -> ( A. x e. X A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) -> ( N ` ( A S B ) ) = ( ( abs ` A ) x. ( N ` B ) ) ) )
21 10 20 syl5 
 |-  ( ( B e. X /\ A e. CC ) -> ( U e. NrmCVec -> ( N ` ( A S B ) ) = ( ( abs ` A ) x. ( N ` B ) ) ) )
22 21 3impia 
 |-  ( ( B e. X /\ A e. CC /\ U e. NrmCVec ) -> ( N ` ( A S B ) ) = ( ( abs ` A ) x. ( N ` B ) ) )
23 22 3com13 
 |-  ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( N ` ( A S B ) ) = ( ( abs ` A ) x. ( N ` B ) ) )