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𝑈 ) = ( 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𝑈 )