Definition df-plp 9364

Description: Define addition on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 9501, and is intended to be used only by the construction. From Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.)

Assertion

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

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

Detailed syntax breakdown of Definition df-plp

Step	Hyp	Ref	Expression
1		cpp 9242	. 2 class +P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 9240	. . 3 class P.
5		vw	. . . . . . . 8 setvar w
6	5	cv 1382	. . . . . . 7 class w
7		vv	. . . . . . . . 9 setvar v
8	7	cv 1382	. . . . . . . 8 class v
9		vu	. . . . . . . . 9 setvar u
10	9	cv 1382	. . . . . . . 8 class u
11		cplq 9236	. . . . . . . 8 class +Q
12	8, 10, 11	co 6281	. . . . . . 7 class ( v +Q u )
13	6, 12	wceq 1383	. . . . . 6 wff w = ( v +Q u )
14	3	cv 1382	. . . . . 6 class y
15	13, 9, 14	wrex 2794	. . . . 5 wff E. u e. y w = ( v +Q u )
16	2	cv 1382	. . . . 5 class x
17	15, 7, 16	wrex 2794	. . . 4 wff E. v e. x E. u e. y w = ( v +Q u )
18	17, 5	cab 2428	. . 3 class { w | E. v e. x E. u e. y w = ( v +Q u ) }
19	2, 3, 4, 4, 18	cmpt2 6283	. 2 class ( x e. P. , y e. P. |-> { w | E. v e. x E. u e. y w = ( v +Q u ) } )
20	1, 19	wceq 1383	1 wff +P. = ( x e. P. , y e. P. |-> { w | E. v e. x E. u e. y w = ( v +Q u ) } )

This definition is referenced by:  plpv  9391  dmplp  9393  addclprlem2  9398  addclpr  9399  addasspr  9403  distrlem1pr  9406  distrlem4pr  9407  distrlem5pr  9408  ltaddpr  9415  ltexprlem6  9422  ltexprlem7  9423