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	⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
	Assertion	cnnvs	⊢ · = ( ·_𝑠OLD ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		cnnvs.6	⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
2		eqid	⊢ ( ·_𝑠OLD ‘ 𝑈 ) = ( ·_𝑠OLD ‘ 𝑈 )
3	2	smfval	⊢ ( ·_𝑠OLD ‘ 𝑈 ) = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) )
4	1	fveq2i	⊢ ( 1^st ‘ 𝑈 ) = ( 1^st ‘ ⟨ ⟨ + , · ⟩ , 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	⊢ ( 1^st ‘ ⟨ ⟨ + , · ⟩ , abs ⟩ ) = ⟨ + , · ⟩
11	4 10	eqtri	⊢ ( 1^st ‘ 𝑈 ) = ⟨ + , · ⟩
12	11	fveq2i	⊢ ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) = ( 2^nd ‘ ⟨ + , · ⟩ )
13		addex	⊢ + ∈ V
14		mulex	⊢ · ∈ V
15	13 14	op2nd	⊢ ( 2^nd ‘ ⟨ + , · ⟩ ) = ·
16	3 12 15	3eqtrri	⊢ · = ( ·_𝑠OLD ‘ 𝑈 )