Definition df-iplp 7583

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

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 7408	. 2 class +P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7406	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1372	. . . . . . . . 9 class r
7	2	cv 1372	. . . . . . . . . 10 class x
8		c1st 6226	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5272	. . . . . . . . 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 5272	. . . . . . . . 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 7397	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 5946	. . . . . . . . 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 7395	. . . . . . 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 6227	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5272	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2176	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5272	. . . . . . . . 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 5948	. 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  7644  addnqpru  7645  addclpr  7652  plpvlu  7653  dmplp  7655  addnqprlemrl  7672  addnqprlemru  7673  addassprg  7694  distrlem1prl  7697  distrlem1pru  7698  distrlem4prl  7699  distrlem4pru  7700  distrlem5prl  7701  distrlem5pru  7702  ltaddpr  7712  ltexprlemfl  7724  ltexprlemrl  7725  ltexprlemfu  7726  ltexprlemru  7727  addcanprleml  7729  addcanprlemu  7730  cauappcvgprlemladdfu  7769  cauappcvgprlemladdfl  7770  caucvgprlemladdfu  7792