Definition df-iplp 7300

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

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 7125	. 2 class +P
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cnp 7123	. . 3 class P
5		vr	. . . . . . . . . 10 setvar 𝑟
6	5	cv 1331	. . . . . . . . 9 class 𝑟
7	2	cv 1331	. . . . . . . . . 10 class 𝑥
8		c1st 6044	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5131	. . . . . . . . 9 class (1st ‘𝑥)
10	6, 9	wcel 1481	. . . . . . . 8 wff 𝑟 ∈ (1st ‘𝑥)
11		vs	. . . . . . . . . 10 setvar 𝑠
12	11	cv 1331	. . . . . . . . 9 class 𝑠
13	3	cv 1331	. . . . . . . . . 10 class 𝑦
14	13, 8	cfv 5131	. . . . . . . . 9 class (1st ‘𝑦)
15	12, 14	wcel 1481	. . . . . . . 8 wff 𝑠 ∈ (1st ‘𝑦)
16		vq	. . . . . . . . . 10 setvar 𝑞
17	16	cv 1331	. . . . . . . . 9 class 𝑞
18		cplq 7114	. . . . . . . . . 10 class +Q
19	6, 12, 18	co 5782	. . . . . . . . 9 class (𝑟 +Q 𝑠)
20	17, 19	wceq 1332	. . . . . . . 8 wff 𝑞 = (𝑟 +Q 𝑠)
21	10, 15, 20	w3a 963	. . . . . . 7 wff (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
22		cnq 7112	. . . . . . 7 class Q
23	21, 11, 22	wrex 2418	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
24	23, 5, 22	wrex 2418	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
25	24, 16, 22	crab 2421	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
26		c2nd 6045	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5131	. . . . . . . . 9 class (2nd ‘𝑥)
28	6, 27	wcel 1481	. . . . . . . 8 wff 𝑟 ∈ (2nd ‘𝑥)
29	13, 26	cfv 5131	. . . . . . . . 9 class (2nd ‘𝑦)
30	12, 29	wcel 1481	. . . . . . . 8 wff 𝑠 ∈ (2nd ‘𝑦)
31	28, 30, 20	w3a 963	. . . . . . 7 wff (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
32	31, 11, 22	wrex 2418	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
33	32, 5, 22	wrex 2418	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
34	33, 16, 22	crab 2421	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
35	25, 34	cop 3535	. . 3 class ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩
36	2, 3, 4, 4, 35	cmpo 5784	. 2 class (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
37	1, 36	wceq 1332	1 wff +P = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)

This definition is referenced by:  addnqprl  7361  addnqpru  7362  addclpr  7369  plpvlu  7370  dmplp  7372  addnqprlemrl  7389  addnqprlemru  7390  addassprg  7411  distrlem1prl  7414  distrlem1pru  7415  distrlem4prl  7416  distrlem4pru  7417  distrlem5prl  7418  distrlem5pru  7419  ltaddpr  7429  ltexprlemfl  7441  ltexprlemrl  7442  ltexprlemfu  7443  ltexprlemru  7444  addcanprleml  7446  addcanprlemu  7447  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  caucvgprlemladdfu  7509