Metamath Proof Explorer


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 = ( BaseSet ` U )
nvzcl.6
|- Z = ( 0vec ` U )
Assertion nvzcl
|- ( U e. NrmCVec -> Z e. X )

Proof

Step Hyp Ref Expression
1 nvzcl.1
 |-  X = ( BaseSet ` U )
2 nvzcl.6
 |-  Z = ( 0vec ` U )
3 eqid
 |-  ( +v ` U ) = ( +v ` U )
4 3 2 0vfval
 |-  ( U e. NrmCVec -> Z = ( GId ` ( +v ` U ) ) )
5 3 nvgrp
 |-  ( U e. NrmCVec -> ( +v ` U ) e. GrpOp )
6 1 3 bafval
 |-  X = ran ( +v ` U )
7 eqid
 |-  ( GId ` ( +v ` U ) ) = ( GId ` ( +v ` U ) )
8 6 7 grpoidcl
 |-  ( ( +v ` U ) e. GrpOp -> ( GId ` ( +v ` U ) ) e. X )
9 5 8 syl
 |-  ( U e. NrmCVec -> ( GId ` ( +v ` U ) ) e. X )
10 4 9 eqeltrd
 |-  ( U e. NrmCVec -> Z e. X )