Definition df-iplp 7601

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, 𝑟 ∈ (1^st ‘𝑥) implies 𝑟 ∈ Q) and can be simplified as shown at genpdf 7641.

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 = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)

Distinct variable group:   𝑥,𝑦,𝑞,𝑟,𝑠

Detailed syntax breakdown of Definition df-iplp

Step	Hyp	Ref	Expression
1		cpp 7426	. 2 class +P
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cnp 7424	. . 3 class P
5		vr	. . . . . . . . . 10 setvar 𝑟
6	5	cv 1372	. . . . . . . . 9 class 𝑟
7	2	cv 1372	. . . . . . . . . 10 class 𝑥
8		c1st 6237	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5280	. . . . . . . . 9 class (1st ‘𝑥)
10	6, 9	wcel 2177	. . . . . . . 8 wff 𝑟 ∈ (1st ‘𝑥)
11		vs	. . . . . . . . . 10 setvar 𝑠
12	11	cv 1372	. . . . . . . . 9 class 𝑠
13	3	cv 1372	. . . . . . . . . 10 class 𝑦
14	13, 8	cfv 5280	. . . . . . . . 9 class (1st ‘𝑦)
15	12, 14	wcel 2177	. . . . . . . 8 wff 𝑠 ∈ (1st ‘𝑦)
16		vq	. . . . . . . . . 10 setvar 𝑞
17	16	cv 1372	. . . . . . . . 9 class 𝑞
18		cplq 7415	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 5957	. . . . . . . . 9 class (𝑟 +Q 𝑠)
20	17, 19	wceq 1373	. . . . . . . 8 wff 𝑞 = (𝑟 +Q 𝑠)
21	10, 15, 20	w3a 981	. . . . . . 7 wff (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
22		cnq 7413	. . . . . . 7 class Q
23	21, 11, 22	wrex 2486	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
24	23, 5, 22	wrex 2486	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
25	24, 16, 22	crab 2489	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
26		c2nd 6238	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5280	. . . . . . . . 9 class (2nd ‘𝑥)
28	6, 27	wcel 2177	. . . . . . . 8 wff 𝑟 ∈ (2nd ‘𝑥)
29	13, 26	cfv 5280	. . . . . . . . 9 class (2nd ‘𝑦)
30	12, 29	wcel 2177	. . . . . . . 8 wff 𝑠 ∈ (2nd ‘𝑦)
31	28, 30, 20	w3a 981	. . . . . . 7 wff (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
32	31, 11, 22	wrex 2486	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
33	32, 5, 22	wrex 2486	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
34	33, 16, 22	crab 2489	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
35	25, 34	cop 3641	. . 3 class ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩
36	2, 3, 4, 4, 35	cmpo 5959	. 2 class (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
37	1, 36	wceq 1373	1 wff +P = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)

This definition is referenced by:  addnqprl  7662  addnqpru  7663  addclpr  7670  plpvlu  7671  dmplp  7673  addnqprlemrl  7690  addnqprlemru  7691  addassprg  7712  distrlem1prl  7715  distrlem1pru  7716  distrlem4prl  7717  distrlem4pru  7718  distrlem5prl  7719  distrlem5pru  7720  ltaddpr  7730  ltexprlemfl  7742  ltexprlemrl  7743  ltexprlemfu  7744  ltexprlemru  7745  addcanprleml  7747  addcanprlemu  7748  cauappcvgprlemladdfu  7787  cauappcvgprlemladdfl  7788  caucvgprlemladdfu  7810