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