Definition df-iplp 6797

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

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 6622	. 2 class +P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 6620	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1284	. . . . . . . . 9 class r
7	2	cv 1284	. . . . . . . . . 10 class x
8		c1st 5818	. . . . . . . . . 10 class 1st
9	7, 8	cfv 4953	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 1434	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1284	. . . . . . . . 9 class s
13	3	cv 1284	. . . . . . . . . 10 class y
14	13, 8	cfv 4953	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 1434	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1284	. . . . . . . . 9 class q
18		cplq 6611	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 5565	. . . . . . . . 9 class ( r +Q s )
20	17, 19	wceq 1285	. . . . . . . 8 wff q = ( r +Q s )
21	10, 15, 20	w3a 920	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
22		cnq 6609	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2354	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
24	23, 5, 22	wrex 2354	. . . . 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 2357	. . . 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 5819	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 4953	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 1434	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 4953	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 1434	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 920	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
32	31, 11, 22	wrex 2354	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
33	32, 5, 22	wrex 2354	. . . . 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 2357	. . . 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 3420	. . 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	cmpt2 5567	. 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 1285	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  6858  addnqpru  6859  addclpr  6866  plpvlu  6867  dmplp  6869  addnqprlemrl  6886  addnqprlemru  6887  addassprg  6908  distrlem1prl  6911  distrlem1pru  6912  distrlem4prl  6913  distrlem4pru  6914  distrlem5prl  6915  distrlem5pru  6916  ltaddpr  6926  ltexprlemfl  6938  ltexprlemrl  6939  ltexprlemfu  6940  ltexprlemru  6941  addcanprleml  6943  addcanprlemu  6944  cauappcvgprlemladdfu  6983  cauappcvgprlemladdfl  6984  caucvgprlemladdfu  7006