Metamath Proof Explorer


Theorem nv0

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

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

Proof

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