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

Metamath Proof Explorer

Theorem cnnvnm

Description: The norm operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypothesis cnnvnm.6 ⊢ U = + × abs
Assertion cnnvnm ⊢ abs = norm CV ⁡ U

Proof

Step Hyp Ref Expression
1 cnnvnm.6 ⊢ U = + × abs
2 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
3 2 nmcvfval ⊢ norm CV ⁡ U = 2 nd ⁡ U
4 1 fveq2i ⊢ 2 nd ⁡ U = 2 nd ⁡ + × 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 op2nd ⊢ 2 nd ⁡ + × abs = abs
11 3 4 10 3eqtrri ⊢ abs = norm CV ⁡ U