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	⊢ 𝑍 = ( 0_vec ‘ 𝑈 )
	Assertion	nvsz	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ) → ( 𝐴 𝑆 𝑍 ) = 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		nvsz.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
2		nvsz.6	⊢ 𝑍 = ( 0_vec ‘ 𝑈 )
3		eqid	⊢ ( 1^st ‘ 𝑈 ) = ( 1^st ‘ 𝑈 )
4	3	nvvc	⊢ ( 𝑈 ∈ NrmCVec → ( 1^st ‘ 𝑈 ) ∈ CVec_OLD )
5		eqid	⊢ ( +_𝑣 ‘ 𝑈 ) = ( +_𝑣 ‘ 𝑈 )
6	5	vafval	⊢ ( +_𝑣 ‘ 𝑈 ) = ( 1^st ‘ ( 1^st ‘ 𝑈 ) )
7	1	smfval	⊢ 𝑆 = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) )
8		eqid	⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
9	8 5	bafval	⊢ ( BaseSet ‘ 𝑈 ) = ran ( +_𝑣 ‘ 𝑈 )
10		eqid	⊢ ( GId ‘ ( +_𝑣 ‘ 𝑈 ) ) = ( GId ‘ ( +_𝑣 ‘ 𝑈 ) )
11	6 7 9 10	vcz	⊢ ( ( ( 1^st ‘ 𝑈 ) ∈ CVec_OLD ∧ 𝐴 ∈ ℂ ) → ( 𝐴 𝑆 ( 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 ∧ 𝐴 ∈ ℂ ) → ( 𝐴 𝑆 𝑍 ) = 𝑍 )