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 | ⊢ 𝑋 = ( BaseSet ‘ 𝑈 ) | |
| nvzcl.6 | ⊢ 𝑍 = ( 0vec ‘ 𝑈 ) | ||
| Assertion | nvzcl | ⊢ ( 𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nvzcl.1 | ⊢ 𝑋 = ( BaseSet ‘ 𝑈 ) | |
| 2 | nvzcl.6 | ⊢ 𝑍 = ( 0vec ‘ 𝑈 ) | |
| 3 | eqid | ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 ) | |
| 4 | 3 2 | 0vfval | ⊢ ( 𝑈 ∈ NrmCVec → 𝑍 = ( GId ‘ ( +𝑣 ‘ 𝑈 ) ) ) |
| 5 | 3 | nvgrp | ⊢ ( 𝑈 ∈ NrmCVec → ( +𝑣 ‘ 𝑈 ) ∈ GrpOp ) |
| 6 | 1 3 | bafval | ⊢ 𝑋 = ran ( +𝑣 ‘ 𝑈 ) |
| 7 | eqid | ⊢ ( GId ‘ ( +𝑣 ‘ 𝑈 ) ) = ( GId ‘ ( +𝑣 ‘ 𝑈 ) ) | |
| 8 | 6 7 | grpoidcl | ⊢ ( ( +𝑣 ‘ 𝑈 ) ∈ GrpOp → ( GId ‘ ( +𝑣 ‘ 𝑈 ) ) ∈ 𝑋 ) |
| 9 | 5 8 | syl | ⊢ ( 𝑈 ∈ NrmCVec → ( GId ‘ ( +𝑣 ‘ 𝑈 ) ) ∈ 𝑋 ) |
| 10 | 4 9 | eqeltrd | ⊢ ( 𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋 ) |