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 = 1 st ⁡ W
vc0.2 ⊢ S = 2 nd ⁡ W
vc0.3 ⊢ X = ran ⁡ G
vc0.4 ⊢ Z = GId ⁡ G
Assertion vcz ⊢ W ∈ CVec OLD ∧ A ∈ ℂ → A S Z = Z

Proof

Step Hyp Ref Expression
1 vc0.1 ⊢ G = 1 st ⁡ W
2 vc0.2 ⊢ S = 2 nd ⁡ W
3 vc0.3 ⊢ X = ran ⁡ G
4 vc0.4 ⊢ Z = GId ⁡ G
5 1 3 4 vczcl ⊢ W ∈ CVec OLD → Z ∈ X
6 5 anim2i ⊢ A ∈ ℂ ∧ W ∈ CVec OLD → A ∈ ℂ ∧ Z ∈ X
7 6 ancoms ⊢ W ∈ CVec OLD ∧ A ∈ ℂ → A ∈ ℂ ∧ Z ∈ X
8 0cn ⊢ 0 ∈ ℂ
9 1 2 3 vcass ⊢ W ∈ CVec OLD ∧ A ∈ ℂ ∧ 0 ∈ ℂ ∧ Z ∈ X → A ⋅ 0 S Z = A S 0 S Z
10 8 9 mp3anr2 ⊢ W ∈ CVec OLD ∧ A ∈ ℂ ∧ Z ∈ X → A ⋅ 0 S Z = A S 0 S Z
11 7 10 syldan ⊢ W ∈ CVec OLD ∧ A ∈ ℂ → A ⋅ 0 S Z = A S 0 S Z
12 mul01 ⊢ A ∈ ℂ → A ⋅ 0 = 0
13 12 oveq1d ⊢ A ∈ ℂ → A ⋅ 0 S Z = 0 S Z
14 1 2 3 4 vc0 ⊢ W ∈ CVec OLD ∧ Z ∈ X → 0 S Z = Z
15 5 14 mpdan ⊢ W ∈ CVec OLD → 0 S Z = Z
16 13 15 sylan9eqr ⊢ W ∈ CVec OLD ∧ A ∈ ℂ → A ⋅ 0 S Z = Z
17 15 oveq2d ⊢ W ∈ CVec OLD → A S 0 S Z = A S Z
18 17 adantr ⊢ W ∈ CVec OLD ∧ A ∈ ℂ → A S 0 S Z = A S Z
19 11 16 18 3eqtr3rd ⊢ W ∈ CVec OLD ∧ A ∈ ℂ → A S Z = Z