# Metamath Proof Explorer

## Theorem cnnvs

Description: The scalar product operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypothesis cnnvs.6 ${⊢}{U}=⟨⟨+,×⟩,\mathrm{abs}⟩$
Assertion cnnvs ${⊢}×={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$

### Proof

Step Hyp Ref Expression
1 cnnvs.6 ${⊢}{U}=⟨⟨+,×⟩,\mathrm{abs}⟩$
2 eqid ${⊢}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
3 2 smfval ${⊢}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)={2}^{nd}\left({1}^{st}\left({U}\right)\right)$
4 1 fveq2i ${⊢}{1}^{st}\left({U}\right)={1}^{st}\left(⟨⟨+,×⟩,\mathrm{abs}⟩\right)$
5 opex ${⊢}⟨+,×⟩\in \mathrm{V}$
6 absf ${⊢}\mathrm{abs}:ℂ⟶ℝ$
7 cnex ${⊢}ℂ\in \mathrm{V}$
8 fex ${⊢}\left(\mathrm{abs}:ℂ⟶ℝ\wedge ℂ\in \mathrm{V}\right)\to \mathrm{abs}\in \mathrm{V}$
9 6 7 8 mp2an ${⊢}\mathrm{abs}\in \mathrm{V}$
10 5 9 op1st ${⊢}{1}^{st}\left(⟨⟨+,×⟩,\mathrm{abs}⟩\right)=⟨+,×⟩$
11 4 10 eqtri ${⊢}{1}^{st}\left({U}\right)=⟨+,×⟩$
12 11 fveq2i ${⊢}{2}^{nd}\left({1}^{st}\left({U}\right)\right)={2}^{nd}\left(⟨+,×⟩\right)$
13 addex ${⊢}+\in \mathrm{V}$
14 mulex ${⊢}×\in \mathrm{V}$
15 13 14 op2nd ${⊢}{2}^{nd}\left(⟨+,×⟩\right)=×$
16 3 12 15 3eqtrri ${⊢}×={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$