Metamath Proof Explorer

Definition df-add

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

Ref Expression
Assertion 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 ) >. ) ) }

Detailed syntax breakdown

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