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 )