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

Metamath Proof Explorer

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 )