This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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⟩, abs⟩$
	Assertion	cnnvg	$⊢ + = +_{v} (U)$

Proof

Step	Hyp	Ref	Expression
1		cnnvg.6	$⊢ U = ⟨⟨+ \times⟩, abs⟩$
2		eqid	$⊢ +_{v} (U) = +_{v} (U)$
3	2	vafval	$⊢ +_{v} (U) = 1^{st} (1^{st} (U))$
4	1	fveq2i	$⊢ 1^{st} (U) = 1^{st} (⟨⟨+ \times⟩, abs⟩)$
5		opex	$⊢ ⟨+ \times⟩ \in V$
6		absf	$⊢ abs : ℂ ⟶ ℝ$
7		cnex	$⊢ ℂ \in V$
8		fex	$⊢ (abs : ℂ ⟶ ℝ \land ℂ \in V) \to abs \in V$
9	6 7 8	mp2an	$⊢ abs \in V$
10	5 9	op1st	$⊢ 1^{st} (⟨⟨+ \times⟩, abs⟩) = ⟨+ \times⟩$
11	4 10	eqtri	$⊢ 1^{st} (U) = ⟨+ \times⟩$
12	11	fveq2i	$⊢ 1^{st} (1^{st} (U)) = 1^{st} (⟨+ \times⟩)$
13		addex	$⊢ + \in V$
14		mulex	$⊢ \times \in V$
15	13 14	op1st	$⊢ 1^{st} (⟨+ \times⟩) = +$
16	3 12 15	3eqtrri	$⊢ + = +_{v} (U)$