Definition df-iplp 7177

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

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 7002	. 2 class +P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7000	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1298	. . . . . . . . 9 class r
7	2	cv 1298	. . . . . . . . . 10 class x
8		c1st 5967	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5059	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 1448	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1298	. . . . . . . . 9 class s
13	3	cv 1298	. . . . . . . . . 10 class y
14	13, 8	cfv 5059	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 1448	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1298	. . . . . . . . 9 class q
18		cplq 6991	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 5706	. . . . . . . . 9 class ( r +Q s )
20	17, 19	wceq 1299	. . . . . . . 8 wff q = ( r +Q s )
21	10, 15, 20	w3a 930	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
22		cnq 6989	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2376	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
24	23, 5, 22	wrex 2376	. . . . 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 2379	. . . 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 5968	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5059	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 1448	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5059	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 1448	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 930	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
32	31, 11, 22	wrex 2376	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
33	32, 5, 22	wrex 2376	. . . . 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 2379	. . . 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 3477	. . 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 5708	. 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 1299	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  7238  addnqpru  7239  addclpr  7246  plpvlu  7247  dmplp  7249  addnqprlemrl  7266  addnqprlemru  7267  addassprg  7288  distrlem1prl  7291  distrlem1pru  7292  distrlem4prl  7293  distrlem4pru  7294  distrlem5prl  7295  distrlem5pru  7296  ltaddpr  7306  ltexprlemfl  7318  ltexprlemrl  7319  ltexprlemfu  7320  ltexprlemru  7321  addcanprleml  7323  addcanprlemu  7324  cauappcvgprlemladdfu  7363  cauappcvgprlemladdfl  7364  caucvgprlemladdfu  7386