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	⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
	Assertion	cnnvnm	⊢ abs = ( norm_CV ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		cnnvnm.6	⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
2		eqid	⊢ ( norm_CV ‘ 𝑈 ) = ( norm_CV ‘ 𝑈 )
3	2	nmcvfval	⊢ ( norm_CV ‘ 𝑈 ) = ( 2^nd ‘ 𝑈 )
4	1	fveq2i	⊢ ( 2^nd ‘ 𝑈 ) = ( 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 ‘ 𝑈 )