Definition df-iplp 7581

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

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 7406	. 2 class +P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7404	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1372	. . . . . . . . 9 class r
7	2	cv 1372	. . . . . . . . . 10 class x
8		c1st 6224	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5271	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2176	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1372	. . . . . . . . 9 class s
13	3	cv 1372	. . . . . . . . . 10 class y
14	13, 8	cfv 5271	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2176	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1372	. . . . . . . . 9 class q
18		cplq 7395	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 5944	. . . . . . . . 9 class ( r +Q s )
20	17, 19	wceq 1373	. . . . . . . 8 wff q = ( r +Q s )
21	10, 15, 20	w3a 981	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
22		cnq 7393	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2485	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
24	23, 5, 22	wrex 2485	. . . . 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 2488	. . . 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 6225	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5271	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2176	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5271	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2176	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 981	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
32	31, 11, 22	wrex 2485	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
33	32, 5, 22	wrex 2485	. . . . 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 2488	. . . 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 3636	. . 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 5946	. 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 1373	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  7642  addnqpru  7643  addclpr  7650  plpvlu  7651  dmplp  7653  addnqprlemrl  7670  addnqprlemru  7671  addassprg  7692  distrlem1prl  7695  distrlem1pru  7696  distrlem4prl  7697  distrlem4pru  7698  distrlem5prl  7699  distrlem5pru  7700  ltaddpr  7710  ltexprlemfl  7722  ltexprlemrl  7723  ltexprlemfu  7724  ltexprlemru  7725  addcanprleml  7727  addcanprlemu  7728  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  caucvgprlemladdfu  7790