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 ‘ 𝑈 ) = ( 2nd ‘ ( 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	⊢ ( 2nd ‘ ( 1st ‘ 𝑈 ) ) = ( 2nd ‘ ⟨ + , · ⟩ )
13		addex	⊢ + ∈ V
14		mulex	⊢ · ∈ V
15	13 14	op2nd	⊢ ( 2nd ‘ ⟨ + , · ⟩ ) = ·
16	3 12 15	3eqtrri	⊢ · = ( ·𝑠OLD ‘ 𝑈 )