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 𝑋 = ( BaseSet ‘ 𝑈 )
nv0.4 𝑆 = ( ·𝑠OLD𝑈 )
nv0.6 𝑍 = ( 0vec𝑈 )
Assertion nv0 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 0 𝑆 𝐴 ) = 𝑍 )

Proof

Step Hyp Ref Expression
1 nv0.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 nv0.4 𝑆 = ( ·𝑠OLD𝑈 )
3 nv0.6 𝑍 = ( 0vec𝑈 )
4 eqid ( 1st𝑈 ) = ( 1st𝑈 )
5 4 nvvc ( 𝑈 ∈ NrmCVec → ( 1st𝑈 ) ∈ CVecOLD )
6 eqid ( +𝑣𝑈 ) = ( +𝑣𝑈 )
7 6 vafval ( +𝑣𝑈 ) = ( 1st ‘ ( 1st𝑈 ) )
8 2 smfval 𝑆 = ( 2nd ‘ ( 1st𝑈 ) )
9 1 6 bafval 𝑋 = ran ( +𝑣𝑈 )
10 eqid ( GId ‘ ( +𝑣𝑈 ) ) = ( GId ‘ ( +𝑣𝑈 ) )
11 7 8 9 10 vc0 ( ( ( 1st𝑈 ) ∈ CVecOLD𝐴𝑋 ) → ( 0 𝑆 𝐴 ) = ( GId ‘ ( +𝑣𝑈 ) ) )
12 5 11 sylan ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 0 𝑆 𝐴 ) = ( GId ‘ ( +𝑣𝑈 ) ) )
13 6 3 0vfval ( 𝑈 ∈ NrmCVec → 𝑍 = ( GId ‘ ( +𝑣𝑈 ) ) )
14 13 adantr ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → 𝑍 = ( GId ‘ ( +𝑣𝑈 ) ) )
15 12 14 eqtr4d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ) → ( 0 𝑆 𝐴 ) = 𝑍 )