This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )