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 𝑆 = ( ·𝑠OLD𝑈 )
nvsz.6 𝑍 = ( 0vec𝑈 )
Assertion nvsz ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ) → ( 𝐴 𝑆 𝑍 ) = 𝑍 )

Proof

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