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=⟨⟨+,\times ⟩,\mathrm{abs}⟩$$
Assertion	cnnvs	$$⊢\times ={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnnvs.6	$$⊢U=⟨⟨+,\times ⟩,\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(⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)$$
5		opex	$$⊢⟨+,\times ⟩\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(⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)=⟨+,\times ⟩$$
11	4 10	eqtri	$$⊢1^{st}\left(U\right)=⟨+,\times ⟩$$
12	11	fveq2i	$$⊢2^{nd}\left(1^{st}\left(U\right)\right)=2^{nd}\left(⟨+,\times ⟩\right)$$
13		addex	$$⊢+\in \mathrm{V}$$
14		mulex	$$⊢\times \in \mathrm{V}$$
15	13 14	op2nd	$$⊢2^{nd}\left(⟨+,\times ⟩\right)=\times$$
16	3 12 15	3eqtrri	$$⊢\times ={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$