Definition df-iplp 7655

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

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 7480	. 2 class +P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7478	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1394	. . . . . . . . 9 class r
7	2	cv 1394	. . . . . . . . . 10 class x
8		c1st 6284	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5318	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2200	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1394	. . . . . . . . 9 class s
13	3	cv 1394	. . . . . . . . . 10 class y
14	13, 8	cfv 5318	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2200	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1394	. . . . . . . . 9 class q
18		cplq 7469	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 6001	. . . . . . . . 9 class ( r +Q s )
20	17, 19	wceq 1395	. . . . . . . 8 wff q = ( r +Q s )
21	10, 15, 20	w3a 1002	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
22		cnq 7467	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2509	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
24	23, 5, 22	wrex 2509	. . . . 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 2512	. . . 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 6285	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5318	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2200	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5318	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2200	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 1002	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
32	31, 11, 22	wrex 2509	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
33	32, 5, 22	wrex 2509	. . . . 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 2512	. . . 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 3669	. . 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 6003	. 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 1395	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  7716  addnqpru  7717  addclpr  7724  plpvlu  7725  dmplp  7727  addnqprlemrl  7744  addnqprlemru  7745  addassprg  7766  distrlem1prl  7769  distrlem1pru  7770  distrlem4prl  7771  distrlem4pru  7772  distrlem5prl  7773  distrlem5pru  7774  ltaddpr  7784  ltexprlemfl  7796  ltexprlemrl  7797  ltexprlemfu  7798  ltexprlemru  7799  addcanprleml  7801  addcanprlemu  7802  cauappcvgprlemladdfu  7841  cauappcvgprlemladdfl  7842  caucvgprlemladdfu  7864