Definition df-iplp 7528

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

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 7353	. 2 class +P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7351	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1363	. . . . . . . . 9 class r
7	2	cv 1363	. . . . . . . . . 10 class x
8		c1st 6191	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5254	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2164	. . . . . . . 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 5254	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2164	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1363	. . . . . . . . 9 class q
18		cplq 7342	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 5918	. . . . . . . . 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 7340	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2473	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
24	23, 5, 22	wrex 2473	. . . . 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 2476	. . . 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 6192	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5254	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2164	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5254	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2164	. . . . . . . 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 2473	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
33	32, 5, 22	wrex 2473	. . . . 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 2476	. . . 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 3621	. . 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 5920	. 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  7589  addnqpru  7590  addclpr  7597  plpvlu  7598  dmplp  7600  addnqprlemrl  7617  addnqprlemru  7618  addassprg  7639  distrlem1prl  7642  distrlem1pru  7643  distrlem4prl  7644  distrlem4pru  7645  distrlem5prl  7646  distrlem5pru  7647  ltaddpr  7657  ltexprlemfl  7669  ltexprlemrl  7670  ltexprlemfu  7671  ltexprlemru  7672  addcanprleml  7674  addcanprlemu  7675  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  caucvgprlemladdfu  7737