Definition df-iplp 7825

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

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 7650	. 2 class +P
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cnp 7648	. . 3 class P
5		vr	. . . . . . . . . 10 setvar 𝑟
6	5	cv 1401	. . . . . . . . 9 class 𝑟
7	2	cv 1401	. . . . . . . . . 10 class 𝑥
8		c1st 6362	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5372	. . . . . . . . 9 class (1st ‘𝑥)
10	6, 9	wcel 2209	. . . . . . . 8 wff 𝑟 ∈ (1st ‘𝑥)
11		vs	. . . . . . . . . 10 setvar 𝑠
12	11	cv 1401	. . . . . . . . 9 class 𝑠
13	3	cv 1401	. . . . . . . . . 10 class 𝑦
14	13, 8	cfv 5372	. . . . . . . . 9 class (1st ‘𝑦)
15	12, 14	wcel 2209	. . . . . . . 8 wff 𝑠 ∈ (1st ‘𝑦)
16		vq	. . . . . . . . . 10 setvar 𝑞
17	16	cv 1401	. . . . . . . . 9 class 𝑞
18		cplq 7639	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 6075	. . . . . . . . 9 class (𝑟 +Q 𝑠)
20	17, 19	wceq 1402	. . . . . . . 8 wff 𝑞 = (𝑟 +Q 𝑠)
21	10, 15, 20	w3a 1009	. . . . . . 7 wff (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
22		cnq 7637	. . . . . . 7 class Q
23	21, 11, 22	wrex 2529	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
24	23, 5, 22	wrex 2529	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
25	24, 16, 22	crab 2532	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
26		c2nd 6363	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5372	. . . . . . . . 9 class (2nd ‘𝑥)
28	6, 27	wcel 2209	. . . . . . . 8 wff 𝑟 ∈ (2nd ‘𝑥)
29	13, 26	cfv 5372	. . . . . . . . 9 class (2nd ‘𝑦)
30	12, 29	wcel 2209	. . . . . . . 8 wff 𝑠 ∈ (2nd ‘𝑦)
31	28, 30, 20	w3a 1009	. . . . . . 7 wff (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
32	31, 11, 22	wrex 2529	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
33	32, 5, 22	wrex 2529	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
34	33, 16, 22	crab 2532	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
35	25, 34	cop 3708	. . 3 class ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩
36	2, 3, 4, 4, 35	cmpo 6077	. 2 class (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
37	1, 36	wceq 1402	1 wff +P = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)

This definition is referenced by:  addnqprl  7886  addnqpru  7887  addclpr  7894  plpvlu  7895  dmplp  7897  addnqprlemrl  7914  addnqprlemru  7915  addassprg  7936  distrlem1prl  7939  distrlem1pru  7940  distrlem4prl  7941  distrlem4pru  7942  distrlem5prl  7943  distrlem5pru  7944  ltaddpr  7954  ltexprlemfl  7966  ltexprlemrl  7967  ltexprlemfu  7968  ltexprlemru  7969  addcanprleml  7971  addcanprlemu  7972  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  caucvgprlemladdfu  8034