Theorem cnnvg

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

	Ref	Expression
Hypothesis	cnnvg.6	$$⊢U=⟨⟨+,\times ⟩,\mathrm{abs}⟩$$
Assertion	cnnvg	$$⊢+={+}_v\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnnvg.6	$$⊢U=⟨⟨+,\times ⟩,\mathrm{abs}⟩$$
2		eqid	$$⊢{+}_v\left(U\right)={+}_v\left(U\right)$$
3	2	vafval	$$⊢{+}_v\left(U\right)=1^{st}\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	$$⊢1^{st}\left(1^{st}\left(U\right)\right)=1^{st}\left(⟨+,\times ⟩\right)$$
13		addex	$$⊢+\in \mathrm{V}$$
14		mulex	$$⊢\times \in \mathrm{V}$$
15	13 14	op1st	$$⊢1^{st}\left(⟨+,\times ⟩\right)=+$$
16	3 12 15	3eqtrri	$$⊢+={+}_v\left(U\right)$$