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 )