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 ) |
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 ) |