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

Proof

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