Definition df-iplp 7269

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

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 7094	. 2 class +P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7092	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1330	. . . . . . . . 9 class r
7	2	cv 1330	. . . . . . . . . 10 class x
8		c1st 6029	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5118	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 1480	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1330	. . . . . . . . 9 class s
13	3	cv 1330	. . . . . . . . . 10 class y
14	13, 8	cfv 5118	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 1480	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1330	. . . . . . . . 9 class q
18		cplq 7083	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 5767	. . . . . . . . 9 class ( r +Q s )
20	17, 19	wceq 1331	. . . . . . . 8 wff q = ( r +Q s )
21	10, 15, 20	w3a 962	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
22		cnq 7081	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2415	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
24	23, 5, 22	wrex 2415	. . . . 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 2418	. . . 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 6030	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5118	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 1480	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5118	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 1480	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 962	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
32	31, 11, 22	wrex 2415	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
33	32, 5, 22	wrex 2415	. . . . 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 2418	. . . 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 3525	. . 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 5769	. 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 1331	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  7330  addnqpru  7331  addclpr  7338  plpvlu  7339  dmplp  7341  addnqprlemrl  7358  addnqprlemru  7359  addassprg  7380  distrlem1prl  7383  distrlem1pru  7384  distrlem4prl  7385  distrlem4pru  7386  distrlem5prl  7387  distrlem5pru  7388  ltaddpr  7398  ltexprlemfl  7410  ltexprlemrl  7411  ltexprlemfu  7412  ltexprlemru  7413  addcanprleml  7415  addcanprlemu  7416  cauappcvgprlemladdfu  7455  cauappcvgprlemladdfl  7456  caucvgprlemladdfu  7478