Definition df-add 9947

Description: Define addition over complex numbers. (Contributed by NM, 28-May-1995.) (New usage is discouraged.)

Assertion

Ref	Expression
df-add	|- + = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) }

Distinct variable group:   x, y, z, w, v, u, f

Detailed syntax breakdown of Definition df-add

Step	Hyp	Ref	Expression
1		caddc 9939	. 2 class +
2		vx	. . . . . . 7 setvar x
3	2	cv 1482	. . . . . 6 class x
4		cc 9934	. . . . . 6 class CC
5	3, 4	wcel 1990	. . . . 5 wff x e. CC
6		vy	. . . . . . 7 setvar y
7	6	cv 1482	. . . . . 6 class y
8	7, 4	wcel 1990	. . . . 5 wff y e. CC
9	5, 8	wa 384	. . . 4 wff ( x e. CC /\ y e. CC )
10		vw	. . . . . . . . . . . . 13 setvar w
11	10	cv 1482	. . . . . . . . . . . 12 class w
12		vv	. . . . . . . . . . . . 13 setvar v
13	12	cv 1482	. . . . . . . . . . . 12 class v
14	11, 13	cop 4183	. . . . . . . . . . 11 class <. w , v >.
15	3, 14	wceq 1483	. . . . . . . . . 10 wff x = <. w , v >.
16		vu	. . . . . . . . . . . . 13 setvar u
17	16	cv 1482	. . . . . . . . . . . 12 class u
18		vf	. . . . . . . . . . . . 13 setvar f
19	18	cv 1482	. . . . . . . . . . . 12 class f
20	17, 19	cop 4183	. . . . . . . . . . 11 class <. u , f >.
21	7, 20	wceq 1483	. . . . . . . . . 10 wff y = <. u , f >.
22	15, 21	wa 384	. . . . . . . . 9 wff ( x = <. w , v >. /\ y = <. u , f >. )
23		vz	. . . . . . . . . . 11 setvar z
24	23	cv 1482	. . . . . . . . . 10 class z
25		cplr 9691	. . . . . . . . . . . 12 class +R
26	11, 17, 25	co 6650	. . . . . . . . . . 11 class ( w +R u )
27	13, 19, 25	co 6650	. . . . . . . . . . 11 class ( v +R f )
28	26, 27	cop 4183	. . . . . . . . . 10 class <. ( w +R u ) , ( v +R f ) >.
29	24, 28	wceq 1483	. . . . . . . . 9 wff z = <. ( w +R u ) , ( v +R f ) >.
30	22, 29	wa 384	. . . . . . . 8 wff ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. )
31	30, 18	wex 1704	. . . . . . 7 wff E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. )
32	31, 16	wex 1704	. . . . . 6 wff E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. )
33	32, 12	wex 1704	. . . . 5 wff E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. )
34	33, 10	wex 1704	. . . 4 wff E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. )
35	9, 34	wa 384	. . 3 wff ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) )
36	35, 2, 6, 23	coprab 6651	. 2 class { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) }
37	1, 36	wceq 1483	1 wff + = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) }

This definition is referenced by:  addcnsr  9956  axaddf  9966