Theorem cnfldnm

Description: The norm of the field of complex numbers. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Assertion	cnfldnm	⊢ abs = ( norm ‘ ℂfld )

Proof

Step	Hyp	Ref	Expression
1		0cn	⊢ 0 ∈ ℂ
2		eqid	⊢ ( abs ∘ − ) = ( abs ∘ − )
3	2	cnmetdval	⊢ ( ( 𝑥 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑥 − 0 ) ) )
4	1 3	mpan2	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑥 − 0 ) ) )
5		subid1	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 − 0 ) = 𝑥 )
6	5	fveq2d	⊢ ( 𝑥 ∈ ℂ → ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ 𝑥 ) )
7	4 6	eqtrd	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ( abs ∘ − ) 0 ) = ( abs ‘ 𝑥 ) )
8	7	mpteq2ia	⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ( abs ∘ − ) 0 ) ) = ( 𝑥 ∈ ℂ ↦ ( abs ‘ 𝑥 ) )
9		eqid	⊢ ( norm ‘ ℂfld ) = ( norm ‘ ℂfld )
10		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
11		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
12		cnfldds	⊢ ( abs ∘ − ) = ( dist ‘ ℂfld )
13	9 10 11 12	nmfval	⊢ ( norm ‘ ℂfld ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ( abs ∘ − ) 0 ) )
14		absf	⊢ abs : ℂ ⟶ ℝ
15	14	a1i	⊢ ( ⊤ → abs : ℂ ⟶ ℝ )
16	15	feqmptd	⊢ ( ⊤ → abs = ( 𝑥 ∈ ℂ ↦ ( abs ‘ 𝑥 ) ) )
17	16	mptru	⊢ abs = ( 𝑥 ∈ ℂ ↦ ( abs ‘ 𝑥 ) )
18	8 13 17	3eqtr4ri	⊢ abs = ( norm ‘ ℂfld )