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 )