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 = BaseSet (U)$
	nvzcl.6	$⊢ Z = 0_{vec} (U)$
Assertion	nvzcl	$⊢ U \in NrmCVec \to Z \in X$

Proof

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

Metamath Proof Explorer

Theorem nvzcl

Proof