Definition df-iplp 7535

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

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 7360	. 2 class +P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7358	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1363	. . . . . . . . 9 class r
7	2	cv 1363	. . . . . . . . . 10 class x
8		c1st 6196	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5258	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2167	. . . . . . . 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 5258	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2167	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1363	. . . . . . . . 9 class q
18		cplq 7349	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 5922	. . . . . . . . 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 7347	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2476	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
24	23, 5, 22	wrex 2476	. . . . 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 2479	. . . 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 6197	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5258	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2167	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5258	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2167	. . . . . . . 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 2476	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
33	32, 5, 22	wrex 2476	. . . . 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 2479	. . . 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 3625	. . 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 5924	. 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  7596  addnqpru  7597  addclpr  7604  plpvlu  7605  dmplp  7607  addnqprlemrl  7624  addnqprlemru  7625  addassprg  7646  distrlem1prl  7649  distrlem1pru  7650  distrlem4prl  7651  distrlem4pru  7652  distrlem5prl  7653  distrlem5pru  7654  ltaddpr  7664  ltexprlemfl  7676  ltexprlemrl  7677  ltexprlemfu  7678  ltexprlemru  7679  addcanprleml  7681  addcanprlemu  7682  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  caucvgprlemladdfu  7744