Definition df-iplp 7430

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

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 7255	. 2 class +P
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cnp 7253	. . 3 class P
5		vr	. . . . . . . . . 10 setvar 𝑟
6	5	cv 1347	. . . . . . . . 9 class 𝑟
7	2	cv 1347	. . . . . . . . . 10 class 𝑥
8		c1st 6117	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5198	. . . . . . . . 9 class (1st ‘𝑥)
10	6, 9	wcel 2141	. . . . . . . 8 wff 𝑟 ∈ (1st ‘𝑥)
11		vs	. . . . . . . . . 10 setvar 𝑠
12	11	cv 1347	. . . . . . . . 9 class 𝑠
13	3	cv 1347	. . . . . . . . . 10 class 𝑦
14	13, 8	cfv 5198	. . . . . . . . 9 class (1st ‘𝑦)
15	12, 14	wcel 2141	. . . . . . . 8 wff 𝑠 ∈ (1st ‘𝑦)
16		vq	. . . . . . . . . 10 setvar 𝑞
17	16	cv 1347	. . . . . . . . 9 class 𝑞
18		cplq 7244	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 5853	. . . . . . . . 9 class (𝑟 +Q 𝑠)
20	17, 19	wceq 1348	. . . . . . . 8 wff 𝑞 = (𝑟 +Q 𝑠)
21	10, 15, 20	w3a 973	. . . . . . 7 wff (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
22		cnq 7242	. . . . . . 7 class Q
23	21, 11, 22	wrex 2449	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
24	23, 5, 22	wrex 2449	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
25	24, 16, 22	crab 2452	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
26		c2nd 6118	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5198	. . . . . . . . 9 class (2nd ‘𝑥)
28	6, 27	wcel 2141	. . . . . . . 8 wff 𝑟 ∈ (2nd ‘𝑥)
29	13, 26	cfv 5198	. . . . . . . . 9 class (2nd ‘𝑦)
30	12, 29	wcel 2141	. . . . . . . 8 wff 𝑠 ∈ (2nd ‘𝑦)
31	28, 30, 20	w3a 973	. . . . . . 7 wff (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
32	31, 11, 22	wrex 2449	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
33	32, 5, 22	wrex 2449	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
34	33, 16, 22	crab 2452	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
35	25, 34	cop 3586	. . 3 class ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩
36	2, 3, 4, 4, 35	cmpo 5855	. 2 class (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
37	1, 36	wceq 1348	1 wff +P = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)

This definition is referenced by:  addnqprl  7491  addnqpru  7492  addclpr  7499  plpvlu  7500  dmplp  7502  addnqprlemrl  7519  addnqprlemru  7520  addassprg  7541  distrlem1prl  7544  distrlem1pru  7545  distrlem4prl  7546  distrlem4pru  7547  distrlem5prl  7548  distrlem5pru  7549  ltaddpr  7559  ltexprlemfl  7571  ltexprlemrl  7572  ltexprlemfu  7573  ltexprlemru  7574  addcanprleml  7576  addcanprlemu  7577  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  caucvgprlemladdfu  7639