Metamath Proof Explorer


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 )