Definition df-iplp 7400

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

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 7225	. 2 class +P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7223	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1341	. . . . . . . . 9 class r
7	2	cv 1341	. . . . . . . . . 10 class x
8		c1st 6098	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5182	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2135	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1341	. . . . . . . . 9 class s
13	3	cv 1341	. . . . . . . . . 10 class y
14	13, 8	cfv 5182	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2135	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1341	. . . . . . . . 9 class q
18		cplq 7214	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 5836	. . . . . . . . 9 class ( r +Q s )
20	17, 19	wceq 1342	. . . . . . . 8 wff q = ( r +Q s )
21	10, 15, 20	w3a 967	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
22		cnq 7212	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2443	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
24	23, 5, 22	wrex 2443	. . . . 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 2446	. . . 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 6099	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5182	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2135	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5182	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2135	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 967	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
32	31, 11, 22	wrex 2443	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
33	32, 5, 22	wrex 2443	. . . . 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 2446	. . . 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 3573	. . 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 5838	. 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 1342	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  7461  addnqpru  7462  addclpr  7469  plpvlu  7470  dmplp  7472  addnqprlemrl  7489  addnqprlemru  7490  addassprg  7511  distrlem1prl  7514  distrlem1pru  7515  distrlem4prl  7516  distrlem4pru  7517  distrlem5prl  7518  distrlem5pru  7519  ltaddpr  7529  ltexprlemfl  7541  ltexprlemrl  7542  ltexprlemfu  7543  ltexprlemru  7544  addcanprleml  7546  addcanprlemu  7547  cauappcvgprlemladdfu  7586  cauappcvgprlemladdfl  7587  caucvgprlemladdfu  7609