Definition df-iplp 7530

Description: Define addition on positive reals. From Section 11.2.1 of [HoTT], p. (varies). We write this definition to closely resemble the definition in HoTT although some of the conditions are redundant (for example, r e. ( 1st ` x ) implies r e. Q.) and can be simplified as shown at genpdf 7570.

This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 26-Sep-2019.)

Assertion

Ref	Expression
df-iplp	|- +P. = ( x e. P. , y e. P. |-> <. { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) ) } , { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) ) } >. )

Distinct variable group:   x, y, q, r, s

Detailed syntax breakdown of Definition df-iplp

Step	Hyp	Ref	Expression
1		cpp 7355	. 2 class +P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7353	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1363	. . . . . . . . 9 class r
7	2	cv 1363	. . . . . . . . . 10 class x
8		c1st 6193	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5255	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2164	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1363	. . . . . . . . 9 class s
13	3	cv 1363	. . . . . . . . . 10 class y
14	13, 8	cfv 5255	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2164	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1363	. . . . . . . . 9 class q
18		cplq 7344	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 5919	. . . . . . . . 9 class ( r +Q s )
20	17, 19	wceq 1364	. . . . . . . 8 wff q = ( r +Q s )
21	10, 15, 20	w3a 980	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
22		cnq 7342	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2473	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
24	23, 5, 22	wrex 2473	. . . . 5 wff E. r e. Q. E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
25	24, 16, 22	crab 2476	. . . 4 class { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) ) }
26		c2nd 6194	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5255	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2164	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5255	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2164	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 980	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
32	31, 11, 22	wrex 2473	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
33	32, 5, 22	wrex 2473	. . . . 5 wff E. r e. Q. E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
34	33, 16, 22	crab 2476	. . . 4 class { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) ) }
35	25, 34	cop 3622	. . 3 class <. { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) ) } , { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) ) } >.
36	2, 3, 4, 4, 35	cmpo 5921	. 2 class ( x e. P. , y e. P. |-> <. { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) ) } , { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) ) } >. )
37	1, 36	wceq 1364	1 wff +P. = ( x e. P. , y e. P. |-> <. { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) ) } , { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) ) } >. )

This definition is referenced by:  addnqprl  7591  addnqpru  7592  addclpr  7599  plpvlu  7600  dmplp  7602  addnqprlemrl  7619  addnqprlemru  7620  addassprg  7641  distrlem1prl  7644  distrlem1pru  7645  distrlem4prl  7646  distrlem4pru  7647  distrlem5prl  7648  distrlem5pru  7649  ltaddpr  7659  ltexprlemfl  7671  ltexprlemrl  7672  ltexprlemfu  7673  ltexprlemru  7674  addcanprleml  7676  addcanprlemu  7677  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  caucvgprlemladdfu  7739