ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-iplp GIF version

Definition df-iplp 7497
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, 𝑟 ∈ (1st𝑥) implies 𝑟Q) and can be simplified as shown at genpdf 7537.

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
StepHypRef Expression
1 cpp 7322 . 2 class +P
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cnp 7320 . . 3 class P
5 vr . . . . . . . . . 10 setvar 𝑟
65cv 1363 . . . . . . . . 9 class 𝑟
72cv 1363 . . . . . . . . . 10 class 𝑥
8 c1st 6163 . . . . . . . . . 10 class 1st
97, 8cfv 5235 . . . . . . . . 9 class (1st𝑥)
106, 9wcel 2160 . . . . . . . 8 wff 𝑟 ∈ (1st𝑥)
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1363 . . . . . . . . 9 class 𝑠
133cv 1363 . . . . . . . . . 10 class 𝑦
1413, 8cfv 5235 . . . . . . . . 9 class (1st𝑦)
1512, 14wcel 2160 . . . . . . . 8 wff 𝑠 ∈ (1st𝑦)
16 vq . . . . . . . . . 10 setvar 𝑞
1716cv 1363 . . . . . . . . 9 class 𝑞
18 cplq 7311 . . . . . . . . . 10 class +Q
196, 12, 18co 5896 . . . . . . . . 9 class (𝑟 +Q 𝑠)
2017, 19wceq 1364 . . . . . . . 8 wff 𝑞 = (𝑟 +Q 𝑠)
2110, 15, 20w3a 980 . . . . . . 7 wff (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
22 cnq 7309 . . . . . . 7 class Q
2321, 11, 22wrex 2469 . . . . . 6 wff 𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
2423, 5, 22wrex 2469 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
2524, 16, 22crab 2472 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
26 c2nd 6164 . . . . . . . . . 10 class 2nd
277, 26cfv 5235 . . . . . . . . 9 class (2nd𝑥)
286, 27wcel 2160 . . . . . . . 8 wff 𝑟 ∈ (2nd𝑥)
2913, 26cfv 5235 . . . . . . . . 9 class (2nd𝑦)
3012, 29wcel 2160 . . . . . . . 8 wff 𝑠 ∈ (2nd𝑦)
3128, 30, 20w3a 980 . . . . . . 7 wff (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
3231, 11, 22wrex 2469 . . . . . 6 wff 𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
3332, 5, 22wrex 2469 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
3433, 16, 22crab 2472 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
3525, 34cop 3610 . . 3 class ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩
362, 3, 4, 4, 35cmpo 5898 . 2 class (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
371, 36wceq 1364 1 wff +P = (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
Colors of variables: wff set class
This definition is referenced by:  addnqprl  7558  addnqpru  7559  addclpr  7566  plpvlu  7567  dmplp  7569  addnqprlemrl  7586  addnqprlemru  7587  addassprg  7608  distrlem1prl  7611  distrlem1pru  7612  distrlem4prl  7613  distrlem4pru  7614  distrlem5prl  7615  distrlem5pru  7616  ltaddpr  7626  ltexprlemfl  7638  ltexprlemrl  7639  ltexprlemfu  7640  ltexprlemru  7641  addcanprleml  7643  addcanprlemu  7644  cauappcvgprlemladdfu  7683  cauappcvgprlemladdfl  7684  caucvgprlemladdfu  7706
  Copyright terms: Public domain W3C validator