Definition df-iplp 7748

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

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 7573	. 2 class +P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7571	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1397	. . . . . . . . 9 class r
7	2	cv 1397	. . . . . . . . . 10 class x
8		c1st 6310	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5333	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2202	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1397	. . . . . . . . 9 class s
13	3	cv 1397	. . . . . . . . . 10 class y
14	13, 8	cfv 5333	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2202	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1397	. . . . . . . . 9 class q
18		cplq 7562	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 6028	. . . . . . . . 9 class ( r +Q s )
20	17, 19	wceq 1398	. . . . . . . 8 wff q = ( r +Q s )
21	10, 15, 20	w3a 1005	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
22		cnq 7560	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2512	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
24	23, 5, 22	wrex 2512	. . . . 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 2515	. . . 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 6311	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5333	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2202	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5333	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2202	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 1005	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
32	31, 11, 22	wrex 2512	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
33	32, 5, 22	wrex 2512	. . . . 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 2515	. . . 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 3676	. . 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 6030	. 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 1398	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  7809  addnqpru  7810  addclpr  7817  plpvlu  7818  dmplp  7820  addnqprlemrl  7837  addnqprlemru  7838  addassprg  7859  distrlem1prl  7862  distrlem1pru  7863  distrlem4prl  7864  distrlem4pru  7865  distrlem5prl  7866  distrlem5pru  7867  ltaddpr  7877  ltexprlemfl  7889  ltexprlemrl  7890  ltexprlemfu  7891  ltexprlemru  7892  addcanprleml  7894  addcanprlemu  7895  cauappcvgprlemladdfu  7934  cauappcvgprlemladdfl  7935  caucvgprlemladdfu  7957