Definition df-abs

Description: Define the function for the absolute value (modulus) of a complex number. See abscli for its closure and absval or absval2i for its value. For example, ( abs-u 2 ) = 2 ( ex-abs ). (Contributed by NM, 27-Jul-1999)

	Ref	Expression
Assertion	df-abs	⊢ abs = ( 𝑥 ∈ ℂ ↦ ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cabs	⊢ abs
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		csqrt	⊢ √
4	1	cv	⊢ 𝑥
5		cmul	⊢ ·
6		ccj	⊢ ∗
7	4 6	cfv	⊢ ( ∗ ‘ 𝑥 )
8	4 7 5	co	⊢ ( 𝑥 · ( ∗ ‘ 𝑥 ) )
9	8 3	cfv	⊢ ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) )
10	1 2 9	cmpt	⊢ ( 𝑥 ∈ ℂ ↦ ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) )
11	0 10	wceq	⊢ abs = ( 𝑥 ∈ ℂ ↦ ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) )