Definition df-iplp 6623

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

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 6448	. 2 class +P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 6446	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1258	. . . . . . . . 9 class r
7	2	cv 1258	. . . . . . . . . 10 class x
8		c1st 5792	. . . . . . . . . 10 class 1st
9	7, 8	cfv 4929	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 1409	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1258	. . . . . . . . 9 class s
13	3	cv 1258	. . . . . . . . . 10 class y
14	13, 8	cfv 4929	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 1409	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1258	. . . . . . . . 9 class q
18		cplq 6437	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 5539	. . . . . . . . 9 class ( r +Q s )
20	17, 19	wceq 1259	. . . . . . . 8 wff q = ( r +Q s )
21	10, 15, 20	w3a 896	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
22		cnq 6435	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2324	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
24	23, 5, 22	wrex 2324	. . . . 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 2327	. . . 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 5793	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 4929	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 1409	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 4929	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 1409	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 896	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
32	31, 11, 22	wrex 2324	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
33	32, 5, 22	wrex 2324	. . . . 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 2327	. . . 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 3405	. . 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	cmpt2 5541	. 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 1259	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  6684  addnqpru  6685  addclpr  6692  plpvlu  6693  dmplp  6695  addnqprlemrl  6712  addnqprlemru  6713  addassprg  6734  distrlem1prl  6737  distrlem1pru  6738  distrlem4prl  6739  distrlem4pru  6740  distrlem5prl  6741  distrlem5pru  6742  ltaddpr  6752  ltexprlemfl  6764  ltexprlemrl  6765  ltexprlemfu  6766  ltexprlemru  6767  addcanprleml  6769  addcanprlemu  6770  cauappcvgprlemladdfu  6809  cauappcvgprlemladdfl  6810  caucvgprlemladdfu  6832