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

Metamath Proof Explorer

Theorem nvsz

Description: Anything times the zero vector is the zero vector. (Contributed by NM, 28-Nov-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nvsz.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
nvsz.6 ⊢ Z = 0 vec ⁡ U
Assertion nvsz ⊢ U ∈ NrmCVec ∧ A ∈ ℂ → A S Z = Z

Proof

Step Hyp Ref Expression
1 nvsz.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
2 nvsz.6 ⊢ Z = 0 vec ⁡ U
3 eqid ⊢ 1 st ⁡ U = 1 st ⁡ U
4 3 nvvc ⊢ U ∈ NrmCVec → 1 st ⁡ U ∈ CVec OLD
5 eqid ⊢ + v ⁡ U = + v ⁡ U
6 5 vafval ⊢ + v ⁡ U = 1 st ⁡ 1 st ⁡ U
7 1 smfval ⊢ S = 2 nd ⁡ 1 st ⁡ U
8 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
9 8 5 bafval ⊢ BaseSet ⁡ U = ran ⁡ + v ⁡ U
10 eqid ⊢ GId ⁡ + v ⁡ U = GId ⁡ + v ⁡ U
11 6 7 9 10 vcz ⊢ 1 st ⁡ U ∈ CVec OLD ∧ A ∈ ℂ → A S GId ⁡ + v ⁡ U = GId ⁡ + v ⁡ U
12 4 11 sylan ⊢ U ∈ NrmCVec ∧ A ∈ ℂ → A S GId ⁡ + v ⁡ U = GId ⁡ + v ⁡ U
13 5 2 0vfval ⊢ U ∈ NrmCVec → Z = GId ⁡ + v ⁡ U
14 13 adantr ⊢ U ∈ NrmCVec ∧ A ∈ ℂ → Z = GId ⁡ + v ⁡ U
15 14 oveq2d ⊢ U ∈ NrmCVec ∧ A ∈ ℂ → A S Z = A S GId ⁡ + v ⁡ U
16 12 15 14 3eqtr4d ⊢ U ∈ NrmCVec ∧ A ∈ ℂ → A S Z = Z