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

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

Proof

Step	Hyp	Ref	Expression
1		cnnvs.6	$⊢ U = ⟨⟨+ \times⟩, abs⟩$
2		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
3	2	smfval	$⊢ \cdot_{𝑠OLD} (U) = 2^{nd} (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	$⊢ 2^{nd} (1^{st} (U)) = 2^{nd} (⟨+ \times⟩)$
13		addex	$⊢ + \in V$
14		mulex	$⊢ \times \in V$
15	13 14	op2nd	$⊢ 2^{nd} (⟨+ \times⟩) = \times$
16	3 12 15	3eqtrri	$⊢ \times = \cdot_{𝑠OLD} (U)$