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

Metamath Proof Explorer

Theorem nvsz

Description: Anything times the zero vector is the zero vector. (Contributed by NM, 28-Nov-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nvsz.4 
|- S = ( .sOLD ` U )
nvsz.6 
|- Z = ( 0vec ` U )
Assertion nvsz 
|- ( ( U e. NrmCVec /\ A e. CC ) -> ( A S Z ) = Z )

Proof

Step Hyp Ref Expression
1 nvsz.4 
 |-  S = ( .sOLD ` U )
2 nvsz.6 
 |-  Z = ( 0vec ` U )
3 eqid 
 |-  ( 1st ` U ) = ( 1st ` U )
4 3 nvvc 
 |-  ( U e. NrmCVec -> ( 1st ` U ) e. CVecOLD )
5 eqid 
 |-  ( +v ` U ) = ( +v ` U )
6 5 vafval 
 |-  ( +v ` U ) = ( 1st ` ( 1st ` U ) )
7 1 smfval 
 |-  S = ( 2nd ` ( 1st ` U ) )
8 eqid 
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
9 8 5 bafval 
 |-  ( BaseSet ` U ) = ran ( +v ` U )
10 eqid 
 |-  ( GId ` ( +v ` U ) ) = ( GId ` ( +v ` U ) )
11 6 7 9 10 vcz 
 |-  ( ( ( 1st ` U ) e. CVecOLD /\ A e. CC ) -> ( A S ( GId ` ( +v ` U ) ) ) = ( GId ` ( +v ` U ) ) )
12 4 11 sylan 
 |-  ( ( U e. NrmCVec /\ A e. CC ) -> ( A S ( GId ` ( +v ` U ) ) ) = ( GId ` ( +v ` U ) ) )
13 5 2 0vfval 
 |-  ( U e. NrmCVec -> Z = ( GId ` ( +v ` U ) ) )
14 13 adantr 
 |-  ( ( U e. NrmCVec /\ A e. CC ) -> Z = ( GId ` ( +v ` U ) ) )
15 14 oveq2d 
 |-  ( ( U e. NrmCVec /\ A e. CC ) -> ( A S Z ) = ( A S ( GId ` ( +v ` U ) ) ) )
16 12 15 14 3eqtr4d 
 |-  ( ( U e. NrmCVec /\ A e. CC ) -> ( A S Z ) = Z )