HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-plus 7010
Description: Define addition over complex numbers.
Assertion
Ref Expression
df-plus |- + = {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.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-plus
StepHypRef Expression
1 caddc 7002 . 2 class +
2 vx . . . . . . 7 set x
32cv 1456 . . . . . 6 class x
4 cc 6997 . . . . . 6 class CC
53, 4wcel 1459 . . . . 5 wff x e. CC
6 vy . . . . . . 7 set y
76cv 1456 . . . . . 6 class y
87, 4wcel 1459 . . . . 5 wff y e. CC
95, 8wa 382 . . . 4 wff (x e. CC /\ y e. CC)
10 vw . . . . . . . . . . . . 13 set w
1110cv 1456 . . . . . . . . . . . 12 class w
12 vv . . . . . . . . . . . . 13 set v
1312cv 1456 . . . . . . . . . . . 12 class v
1411, 13cop 3100 . . . . . . . . . . 11 class <.w, v>.
153, 14wceq 1457 . . . . . . . . . 10 wff x = <.w, v>.
16 vu . . . . . . . . . . . . 13 set u
1716cv 1456 . . . . . . . . . . . 12 class u
18 vf . . . . . . . . . . . . 13 set f
1918cv 1456 . . . . . . . . . . . 12 class f
2017, 19cop 3100 . . . . . . . . . . 11 class <.u, f>.
217, 20wceq 1457 . . . . . . . . . 10 wff y = <.u, f>.
2215, 21wa 382 . . . . . . . . 9 wff (x = <.w, v>. /\ y = <.u, f>.)
23 vz . . . . . . . . . . 11 set z
2423cv 1456 . . . . . . . . . 10 class z
25 cplr 6753 . . . . . . . . . . . 12 class +R
2611, 17, 25co 4935 . . . . . . . . . . 11 class (w +R u)
2713, 19, 25co 4935 . . . . . . . . . . 11 class (v +R f)
2826, 27cop 3100 . . . . . . . . . 10 class <.(w +R u), (v +R f)>.
2924, 28wceq 1457 . . . . . . . . 9 wff z = <.(w +R u), (v +R f)>.
3022, 29wa 382 . . . . . . . 8 wff ((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.(w +R u), (v +R f)>.)
3130, 18wex 1380 . . . . . . 7 wff E.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.(w +R u), (v +R f)>.)
3231, 16wex 1380 . . . . . 6 wff E.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.(w +R u), (v +R f)>.)
3332, 12wex 1380 . . . . 5 wff E.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.(w +R u), (v +R f)>.)
3433, 10wex 1380 . . . 4 wff E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.(w +R u), (v +R f)>.)
359, 34wa 382 . . 3 wff ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.(w +R u), (v +R f)>.))
3635, 2, 6, 23copab2 4936 . 2 class {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.(w +R u), (v +R f)>.))}
371, 36wceq 1457 1 wff + = {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.(w +R u), (v +R f)>.))}
Colors of variables: wff set class
This definition is referenced by:  addcnsr 7019  axaddopr 7029
Copyright terms: Public domain