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

Metamath Proof Explorer

Theorem nv0

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

Ref Expression
Hypotheses nv0.1 ⊢ X = BaseSet ⁡ U
nv0.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
nv0.6 ⊢ Z = 0 vec ⁡ U
Assertion nv0 ⊢ U ∈ NrmCVec ∧ A ∈ X → 0 S A = Z

Proof

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