Description: The base set of the normed complex vector space of complex numbers. (Contributed by NM, 7-Nov-2007) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cnnvba.6 | ⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩ | |
| Assertion | cnnvba | ⊢ ℂ = ( BaseSet ‘ 𝑈 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnnvba.6 | ⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩ | |
| 2 | 1 | cnnvg | ⊢ + = ( +𝑣 ‘ 𝑈 ) |
| 3 | 2 | rneqi | ⊢ ran + = ran ( +𝑣 ‘ 𝑈 ) |
| 4 | cnaddabloOLD | ⊢ + ∈ AbelOp | |
| 5 | ablogrpo | ⊢ ( + ∈ AbelOp → + ∈ GrpOp ) | |
| 6 | 4 5 | ax-mp | ⊢ + ∈ GrpOp |
| 7 | ax-addf | ⊢ + : ( ℂ × ℂ ) ⟶ ℂ | |
| 8 | 7 | fdmi | ⊢ dom + = ( ℂ × ℂ ) |
| 9 | 6 8 | grporn | ⊢ ℂ = ran + |
| 10 | eqid | ⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 ) | |
| 11 | eqid | ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 ) | |
| 12 | 10 11 | bafval | ⊢ ( BaseSet ‘ 𝑈 ) = ran ( +𝑣 ‘ 𝑈 ) |
| 13 | 3 9 12 | 3eqtr4i | ⊢ ℂ = ( BaseSet ‘ 𝑈 ) |