Theorem vc0

Description: Zero times a vector is the zero vector. Equation 1a of Kreyszig p. 51. (Contributed by NM, 4-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	vc0	|- ( ( W e. CVecOLD /\ A e. X ) -> ( 0 S A ) = 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	vc0rid	|- ( ( W e. CVecOLD /\ A e. X ) -> ( A G Z ) = A )
6		1p0e1	|- ( 1 + 0 ) = 1
7	6	oveq1i	|- ( ( 1 + 0 ) S A ) = ( 1 S A )
8		0cn	|- 0 e. CC
9		ax-1cn	|- 1 e. CC
10	1 2 3	vcdir	|- ( ( W e. CVecOLD /\ ( 1 e. CC /\ 0 e. CC /\ A e. X ) ) -> ( ( 1 + 0 ) S A ) = ( ( 1 S A ) G ( 0 S A ) ) )
11	9 10	mp3anr1	|- ( ( W e. CVecOLD /\ ( 0 e. CC /\ A e. X ) ) -> ( ( 1 + 0 ) S A ) = ( ( 1 S A ) G ( 0 S A ) ) )
12	8 11	mpanr1	|- ( ( W e. CVecOLD /\ A e. X ) -> ( ( 1 + 0 ) S A ) = ( ( 1 S A ) G ( 0 S A ) ) )
13	1 2 3	vcidOLD	|- ( ( W e. CVecOLD /\ A e. X ) -> ( 1 S A ) = A )
14	7 12 13	3eqtr3a	|- ( ( W e. CVecOLD /\ A e. X ) -> ( ( 1 S A ) G ( 0 S A ) ) = A )
15	13	oveq1d	|- ( ( W e. CVecOLD /\ A e. X ) -> ( ( 1 S A ) G ( 0 S A ) ) = ( A G ( 0 S A ) ) )
16	5 14 15	3eqtr2rd	|- ( ( W e. CVecOLD /\ A e. X ) -> ( A G ( 0 S A ) ) = ( A G Z ) )
17	1 2 3	vccl	|- ( ( W e. CVecOLD /\ 0 e. CC /\ A e. X ) -> ( 0 S A ) e. X )
18	8 17	mp3an2	|- ( ( W e. CVecOLD /\ A e. X ) -> ( 0 S A ) e. X )
19	1 3 4	vczcl	|- ( W e. CVecOLD -> Z e. X )
20	19	adantr	|- ( ( W e. CVecOLD /\ A e. X ) -> Z e. X )
21		simpr	|- ( ( W e. CVecOLD /\ A e. X ) -> A e. X )
22	18 20 21	3jca	|- ( ( W e. CVecOLD /\ A e. X ) -> ( ( 0 S A ) e. X /\ Z e. X /\ A e. X ) )
23	1 3	vclcan	|- ( ( W e. CVecOLD /\ ( ( 0 S A ) e. X /\ Z e. X /\ A e. X ) ) -> ( ( A G ( 0 S A ) ) = ( A G Z ) <-> ( 0 S A ) = Z ) )
24	22 23	syldan	|- ( ( W e. CVecOLD /\ A e. X ) -> ( ( A G ( 0 S A ) ) = ( A G Z ) <-> ( 0 S A ) = Z ) )
25	16 24	mpbid	|- ( ( W e. CVecOLD /\ A e. X ) -> ( 0 S A ) = Z )