Theorem nvzcl

Description: Closure law for the zero vector of a normed complex vector space. (Contributed by NM, 27-Nov-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvzcl.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	nvzcl.6	$$⊢Z=0_{\mathrm{vec}}\left(U\right)$$
Assertion	nvzcl	$$⊢U\in \mathrm{NrmCVec}\to Z\in X$$

Proof

Step	Hyp	Ref	Expression
1		nvzcl.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		nvzcl.6	$$⊢Z=0_{\mathrm{vec}}\left(U\right)$$
3		eqid	$$⊢{+}_v\left(U\right)={+}_v\left(U\right)$$
4	3 2	0vfval	$$⊢U\in \mathrm{NrmCVec}\to Z=\mathrm{GId}\left({+}_v\left(U\right)\right)$$
5	3	nvgrp	$$⊢U\in \mathrm{NrmCVec}\to {+}_v\left(U\right)\in \mathrm{GrpOp}$$
6	1 3	bafval	$$⊢X=\mathrm{ran}{+}_v\left(U\right)$$
7		eqid	$$⊢\mathrm{GId}\left({+}_v\left(U\right)\right)=\mathrm{GId}\left({+}_v\left(U\right)\right)$$
8	6 7	grpoidcl	$$⊢{+}_v\left(U\right)\in \mathrm{GrpOp}\to \mathrm{GId}\left({+}_v\left(U\right)\right)\in X$$
9	5 8	syl	$$⊢U\in \mathrm{NrmCVec}\to \mathrm{GId}\left({+}_v\left(U\right)\right)\in X$$
10	4 9	eqeltrd	$$⊢U\in \mathrm{NrmCVec}\to Z\in X$$