Theorem vcz

Description: Anything times the zero vector is the zero vector. Equation 1b of Kreyszig p. 51. (Contributed by NM, 24-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	vc0.1	|- G = ( 1st ` W )
	vc0.2	|- S = ( 2nd ` W )
	vc0.3	|- X = ran G
	vc0.4	|- Z = ( GId ` G )
Assertion	vcz	|- ( ( W e. CVecOLD /\ A e. CC ) -> ( A S Z ) = Z )

Proof

Step	Hyp	Ref	Expression
1		vc0.1	|- G = ( 1st ` W )
2		vc0.2	|- S = ( 2nd ` W )
3		vc0.3	|- X = ran G
4		vc0.4	|- Z = ( GId ` G )
5	1 3 4	vczcl	|- ( W e. CVecOLD -> Z e. X )
6	5	anim2i	|- ( ( A e. CC /\ W e. CVecOLD ) -> ( A e. CC /\ Z e. X ) )
7	6	ancoms	|- ( ( W e. CVecOLD /\ A e. CC ) -> ( A e. CC /\ Z e. X ) )
8		0cn	|- 0 e. CC
9	1 2 3	vcass	|- ( ( W e. CVecOLD /\ ( A e. CC /\ 0 e. CC /\ Z e. X ) ) -> ( ( A x. 0 ) S Z ) = ( A S ( 0 S Z ) ) )
10	8 9	mp3anr2	|- ( ( W e. CVecOLD /\ ( A e. CC /\ Z e. X ) ) -> ( ( A x. 0 ) S Z ) = ( A S ( 0 S Z ) ) )
11	7 10	syldan	|- ( ( W e. CVecOLD /\ A e. CC ) -> ( ( A x. 0 ) S Z ) = ( A S ( 0 S Z ) ) )
12		mul01	|- ( A e. CC -> ( A x. 0 ) = 0 )
13	12	oveq1d	|- ( A e. CC -> ( ( A x. 0 ) S Z ) = ( 0 S Z ) )
14	1 2 3 4	vc0	|- ( ( W e. CVecOLD /\ Z e. X ) -> ( 0 S Z ) = Z )
15	5 14	mpdan	|- ( W e. CVecOLD -> ( 0 S Z ) = Z )
16	13 15	sylan9eqr	|- ( ( W e. CVecOLD /\ A e. CC ) -> ( ( A x. 0 ) S Z ) = Z )
17	15	oveq2d	|- ( W e. CVecOLD -> ( A S ( 0 S Z ) ) = ( A S Z ) )
18	17	adantr	|- ( ( W e. CVecOLD /\ A e. CC ) -> ( A S ( 0 S Z ) ) = ( A S Z ) )
19	11 16 18	3eqtr3rd	|- ( ( W e. CVecOLD /\ A e. CC ) -> ( A S Z ) = Z )