Definition df-plp 6240

Description: Define addition on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 6392, and is intended to be used only by the construction. From Proposition 9-3.5 of [Gleason] p. 123.

Assertion

Ref	Expression
df-plp	|- +P. = {<.<.x, y>., z>. | ((x e. P. /\ y e. P.) /\ z = {w | E.v e. x E.u e. y w = (v +Q u)})}

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

Detailed syntax breakdown of Definition df-plp

Step	Hyp	Ref	Expression
1		cpp 6139	. 2 class +P.
2		vx	. . . . . . 7 set x
3	2	cv 1297	. . . . . 6 class x
4		cnp 6137	. . . . . 6 class P.
5	3, 4	wcel 1300	. . . . 5 wff x e. P.
6		vy	. . . . . . 7 set y
7	6	cv 1297	. . . . . 6 class y
8	7, 4	wcel 1300	. . . . 5 wff y e. P.
9	5, 8	wa 240	. . . 4 wff (x e. P. /\ y e. P.)
10		vz	. . . . . 6 set z
11	10	cv 1297	. . . . 5 class z
12		vw	. . . . . . . . . 10 set w
13	12	cv 1297	. . . . . . . . 9 class w
14		vv	. . . . . . . . . . 11 set v
15	14	cv 1297	. . . . . . . . . 10 class v
16		vu	. . . . . . . . . . 11 set u
17	16	cv 1297	. . . . . . . . . 10 class u
18		cplq 6133	. . . . . . . . . 10 class +Q
19	15, 17, 18	co 4884	. . . . . . . . 9 class (v +Q u)
20	13, 19	wceq 1298	. . . . . . . 8 wff w = (v +Q u)
21	20, 16, 7	wrex 2106	. . . . . . 7 wff E.u e. y w = (v +Q u)
22	21, 14, 3	wrex 2106	. . . . . 6 wff E.v e. x E.u e. y w = (v +Q u)
23	22, 12	cab 1871	. . . . 5 class {w | E.v e. x E.u e. y w = (v +Q u)}
24	11, 23	wceq 1298	. . . 4 wff z = {w | E.v e. x E.u e. y w = (v +Q u)}
25	9, 24	wa 240	. . 3 wff ((x e. P. /\ y e. P.) /\ z = {w | E.v e. x E.u e. y w = (v +Q u)})
26	25, 2, 6, 10	copab2 4885	. 2 class {<.<.x, y>., z>. | ((x e. P. /\ y e. P.) /\ z = {w | E.v e. x E.u e. y w = (v +Q u)})}
27	1, 26	wceq 1298	1 wff +P. = {<.<.x, y>., z>. | ((x e. P. /\ y e. P.) /\ z = {w | E.v e. x E.u e. y w = (v +Q u)})}

This definition is referenced by:  plpv 6265  dmplp 6267  addclprlem2 6271  addclpr 6272  addasspr 6276  distrlem1pr 6279  distrlem2pr 6280  distrlem5pr 6283  ltaddpr 6292  ltexprlem6 6299  ltexprlem7 6300

Copyright terms: Public domain