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	⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
Assertion	cnnvg	⊢ + = ( +𝑣 ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		cnnvg.6	⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
2		eqid	⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
3	2	vafval	⊢ ( +𝑣 ‘ 𝑈 ) = ( 1st ‘ ( 1st ‘ 𝑈 ) )
4	1	fveq2i	⊢ ( 1st ‘ 𝑈 ) = ( 1st ‘ ⟨ ⟨ + , · ⟩ , abs ⟩ )
5		opex	⊢ ⟨ + , · ⟩ ∈ V
6		absf	⊢ abs : ℂ ⟶ ℝ
7		cnex	⊢ ℂ ∈ V
8		fex	⊢ ( ( abs : ℂ ⟶ ℝ ∧ ℂ ∈ V ) → abs ∈ V )
9	6 7 8	mp2an	⊢ abs ∈ V
10	5 9	op1st	⊢ ( 1st ‘ ⟨ ⟨ + , · ⟩ , abs ⟩ ) = ⟨ + , · ⟩
11	4 10	eqtri	⊢ ( 1st ‘ 𝑈 ) = ⟨ + , · ⟩
12	11	fveq2i	⊢ ( 1st ‘ ( 1st ‘ 𝑈 ) ) = ( 1st ‘ ⟨ + , · ⟩ )
13		addex	⊢ + ∈ V
14		mulex	⊢ · ∈ V
15	13 14	op1st	⊢ ( 1st ‘ ⟨ + , · ⟩ ) = +
16	3 12 15	3eqtrri	⊢ + = ( +𝑣 ‘ 𝑈 )