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	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
	nvsz.6	$$⊢Z=0_{\mathrm{vec}}\left(U\right)$$
Assertion	nvsz	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in ℂ\right)\to ASZ=Z$$

Proof

Step	Hyp	Ref	Expression
1		nvsz.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
2		nvsz.6	$$⊢Z=0_{\mathrm{vec}}\left(U\right)$$
3		eqid	$$⊢1^{st}\left(U\right)=1^{st}\left(U\right)$$
4	3	nvvc	$$⊢U\in \mathrm{NrmCVec}\to 1^{st}\left(U\right)\in {CVec}_{\mathrm{OLD}}$$
5		eqid	$$⊢{+}_v\left(U\right)={+}_v\left(U\right)$$
6	5	vafval	$$⊢{+}_v\left(U\right)=1^{st}\left(1^{st}\left(U\right)\right)$$
7	1	smfval	$$⊢S=2^{nd}\left(1^{st}\left(U\right)\right)$$
8		eqid	$$⊢\mathrm{BaseSet}\left(U\right)=\mathrm{BaseSet}\left(U\right)$$
9	8 5	bafval	$$⊢\mathrm{BaseSet}\left(U\right)=\mathrm{ran}{+}_v\left(U\right)$$
10		eqid	$$⊢\mathrm{GId}\left({+}_v\left(U\right)\right)=\mathrm{GId}\left({+}_v\left(U\right)\right)$$
11	6 7 9 10	vcz	$$⊢\left(1^{st}\left(U\right)\in {CVec}_{\mathrm{OLD}}\wedge A\in ℂ\right)\to AS\mathrm{GId}\left({+}_v\left(U\right)\right)=\mathrm{GId}\left({+}_v\left(U\right)\right)$$
12	4 11	sylan	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in ℂ\right)\to AS\mathrm{GId}\left({+}_v\left(U\right)\right)=\mathrm{GId}\left({+}_v\left(U\right)\right)$$
13	5 2	0vfval	$$⊢U\in \mathrm{NrmCVec}\to Z=\mathrm{GId}\left({+}_v\left(U\right)\right)$$
14	13	adantr	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in ℂ\right)\to Z=\mathrm{GId}\left({+}_v\left(U\right)\right)$$
15	14	oveq2d	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in ℂ\right)\to ASZ=AS\mathrm{GId}\left({+}_v\left(U\right)\right)$$
16	12 15 14	3eqtr4d	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in ℂ\right)\to ASZ=Z$$