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 𝐺 = ( 1st𝑊 )
vc0.2 𝑆 = ( 2nd𝑊 )
vc0.3 𝑋 = ran 𝐺
vc0.4 𝑍 = ( GId ‘ 𝐺 )
Assertion vcz ( ( 𝑊 ∈ CVecOLD𝐴 ∈ ℂ ) → ( 𝐴 𝑆 𝑍 ) = 𝑍 )

Proof

Step Hyp Ref Expression
1 vc0.1 𝐺 = ( 1st𝑊 )
2 vc0.2 𝑆 = ( 2nd𝑊 )
3 vc0.3 𝑋 = ran 𝐺
4 vc0.4 𝑍 = ( GId ‘ 𝐺 )
5 1 3 4 vczcl ( 𝑊 ∈ CVecOLD𝑍𝑋 )
6 5 anim2i ( ( 𝐴 ∈ ℂ ∧ 𝑊 ∈ CVecOLD ) → ( 𝐴 ∈ ℂ ∧ 𝑍𝑋 ) )
7 6 ancoms ( ( 𝑊 ∈ CVecOLD𝐴 ∈ ℂ ) → ( 𝐴 ∈ ℂ ∧ 𝑍𝑋 ) )
8 0cn 0 ∈ ℂ
9 1 2 3 vcass ( ( 𝑊 ∈ CVecOLD ∧ ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ∧ 𝑍𝑋 ) ) → ( ( 𝐴 · 0 ) 𝑆 𝑍 ) = ( 𝐴 𝑆 ( 0 𝑆 𝑍 ) ) )
10 8 9 mp3anr2 ( ( 𝑊 ∈ CVecOLD ∧ ( 𝐴 ∈ ℂ ∧ 𝑍𝑋 ) ) → ( ( 𝐴 · 0 ) 𝑆 𝑍 ) = ( 𝐴 𝑆 ( 0 𝑆 𝑍 ) ) )
11 7 10 syldan ( ( 𝑊 ∈ CVecOLD𝐴 ∈ ℂ ) → ( ( 𝐴 · 0 ) 𝑆 𝑍 ) = ( 𝐴 𝑆 ( 0 𝑆 𝑍 ) ) )
12 mul01 ( 𝐴 ∈ ℂ → ( 𝐴 · 0 ) = 0 )
13 12 oveq1d ( 𝐴 ∈ ℂ → ( ( 𝐴 · 0 ) 𝑆 𝑍 ) = ( 0 𝑆 𝑍 ) )
14 1 2 3 4 vc0 ( ( 𝑊 ∈ CVecOLD𝑍𝑋 ) → ( 0 𝑆 𝑍 ) = 𝑍 )
15 5 14 mpdan ( 𝑊 ∈ CVecOLD → ( 0 𝑆 𝑍 ) = 𝑍 )
16 13 15 sylan9eqr ( ( 𝑊 ∈ CVecOLD𝐴 ∈ ℂ ) → ( ( 𝐴 · 0 ) 𝑆 𝑍 ) = 𝑍 )
17 15 oveq2d ( 𝑊 ∈ CVecOLD → ( 𝐴 𝑆 ( 0 𝑆 𝑍 ) ) = ( 𝐴 𝑆 𝑍 ) )
18 17 adantr ( ( 𝑊 ∈ CVecOLD𝐴 ∈ ℂ ) → ( 𝐴 𝑆 ( 0 𝑆 𝑍 ) ) = ( 𝐴 𝑆 𝑍 ) )
19 11 16 18 3eqtr3rd ( ( 𝑊 ∈ CVecOLD𝐴 ∈ ℂ ) → ( 𝐴 𝑆 𝑍 ) = 𝑍 )