Definition df-abs 4793

Description: Define the function for the absolute value (modulus) of a complex number. See abscl 4840 for its closure and absvalt 4801 or absval2 4836 for its value.

Assertion

Ref	Expression
df-abs	|- abs = {<.x, y>. | (x e. CC /\ y = (sqr` (x x. (*` x))))}

Distinct variable group(s):   x,y

Detailed syntax breakdown of Definition df-abs

Step	Hyp	Ref	Expression
1		cabs 4789	. 2 class abs
2		vx	. . . . . 6 set x
3	2	cv 1089	. . . . 5 class x
4		cc 4026	. . . . 5 class CC
5	3, 4	wcel 1092	. . . 4 wff x e. CC
6		vy	. . . . . 6 set y
7	6	cv 1089	. . . . 5 class y
8		ccj 4788	. . . . . . . 8 class *
9	3, 8	cfv 2422	. . . . . . 7 class (*` x)
10		cmulc 4032	. . . . . . 7 class x.
11	3, 9, 10	co 3001	. . . . . 6 class (x x. (*` x))
12		csqr 4727	. . . . . 6 class sqr
13	11, 12	cfv 2422	. . . . 5 class (sqr` (x x. (*` x)))
14	7, 13	wceq 1091	. . . 4 wff y = (sqr` (x x. (*` x)))
15	5, 14	wa 196	. . 3 wff (x e. CC /\ y = (sqr` (x x. (*` x))))
16	15, 2, 6	copab 2055	. 2 class {<.x, y>. | (x e. CC /\ y = (sqr` (x x. (*` x))))}
17	1, 16	wceq 1091	1 wff abs = {<.x, y>. | (x e. CC /\ y = (sqr` (x x. (*` x))))}

This definition is referenced by:  absvalt 4801

metamath.org