Definition df-iplp 7498

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 7538.

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 7323	. 2 class +P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7321	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1363	. . . . . . . . 9 class r
7	2	cv 1363	. . . . . . . . . 10 class x
8		c1st 6164	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5235	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2160	. . . . . . . 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 5235	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2160	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1363	. . . . . . . . 9 class q
18		cplq 7312	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 5897	. . . . . . . . 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 7310	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2469	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
24	23, 5, 22	wrex 2469	. . . . 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 2472	. . . 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 6165	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5235	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2160	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5235	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2160	. . . . . . . 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 2469	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
33	32, 5, 22	wrex 2469	. . . . 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 2472	. . . 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 3610	. . 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 5899	. 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  7559  addnqpru  7560  addclpr  7567  plpvlu  7568  dmplp  7570  addnqprlemrl  7587  addnqprlemru  7588  addassprg  7609  distrlem1prl  7612  distrlem1pru  7613  distrlem4prl  7614  distrlem4pru  7615  distrlem5prl  7616  distrlem5pru  7617  ltaddpr  7627  ltexprlemfl  7639  ltexprlemrl  7640  ltexprlemfu  7641  ltexprlemru  7642  addcanprleml  7644  addcanprlemu  7645  cauappcvgprlemladdfu  7684  cauappcvgprlemladdfl  7685  caucvgprlemladdfu  7707