Definition df-iplp 6971

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

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 6796	. 2 class +P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 6794	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1286	. . . . . . . . 9 class r
7	2	cv 1286	. . . . . . . . . 10 class x
8		c1st 5866	. . . . . . . . . 10 class 1st
9	7, 8	cfv 4981	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 1436	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1286	. . . . . . . . 9 class s
13	3	cv 1286	. . . . . . . . . 10 class y
14	13, 8	cfv 4981	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 1436	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1286	. . . . . . . . 9 class q
18		cplq 6785	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 5613	. . . . . . . . 9 class ( r +Q s )
20	17, 19	wceq 1287	. . . . . . . 8 wff q = ( r +Q s )
21	10, 15, 20	w3a 922	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
22		cnq 6783	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2356	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) )
24	23, 5, 22	wrex 2356	. . . . 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 2359	. . . 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 5867	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 4981	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 1436	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 4981	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 1436	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 922	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
32	31, 11, 22	wrex 2356	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) )
33	32, 5, 22	wrex 2356	. . . . 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 2359	. . . 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 3434	. . 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 5615	. 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 1287	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  7032  addnqpru  7033  addclpr  7040  plpvlu  7041  dmplp  7043  addnqprlemrl  7060  addnqprlemru  7061  addassprg  7082  distrlem1prl  7085  distrlem1pru  7086  distrlem4prl  7087  distrlem4pru  7088  distrlem5prl  7089  distrlem5pru  7090  ltaddpr  7100  ltexprlemfl  7112  ltexprlemrl  7113  ltexprlemfu  7114  ltexprlemru  7115  addcanprleml  7117  addcanprlemu  7118  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  caucvgprlemladdfu  7180