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 ⊢ 𝐺 = ( 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 ∧ 𝐴 ∈ ℂ ) → ( 𝐴 𝑆 𝑍 ) = 𝑍 )