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

Definition df-iplp 7458
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 7498.

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 7283 . 2 class +P
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cnp 7281 . . 3 class P
5 vr . . . . . . . . . 10 setvar 𝑟
65cv 1352 . . . . . . . . 9 class 𝑟
72cv 1352 . . . . . . . . . 10 class 𝑥
8 c1st 6133 . . . . . . . . . 10 class 1st
97, 8cfv 5212 . . . . . . . . 9 class (1st𝑥)
106, 9wcel 2148 . . . . . . . 8 wff 𝑟 ∈ (1st𝑥)
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1352 . . . . . . . . 9 class 𝑠
133cv 1352 . . . . . . . . . 10 class 𝑦
1413, 8cfv 5212 . . . . . . . . 9 class (1st𝑦)
1512, 14wcel 2148 . . . . . . . 8 wff 𝑠 ∈ (1st𝑦)
16 vq . . . . . . . . . 10 setvar 𝑞
1716cv 1352 . . . . . . . . 9 class 𝑞
18 cplq 7272 . . . . . . . . . 10 class +Q
196, 12, 18co 5869 . . . . . . . . 9 class (𝑟 +Q 𝑠)
2017, 19wceq 1353 . . . . . . . 8 wff 𝑞 = (𝑟 +Q 𝑠)
2110, 15, 20w3a 978 . . . . . . 7 wff (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
22 cnq 7270 . . . . . . 7 class Q
2321, 11, 22wrex 2456 . . . . . 6 wff 𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
2423, 5, 22wrex 2456 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
2524, 16, 22crab 2459 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
26 c2nd 6134 . . . . . . . . . 10 class 2nd
277, 26cfv 5212 . . . . . . . . 9 class (2nd𝑥)
286, 27wcel 2148 . . . . . . . 8 wff 𝑟 ∈ (2nd𝑥)
2913, 26cfv 5212 . . . . . . . . 9 class (2nd𝑦)
3012, 29wcel 2148 . . . . . . . 8 wff 𝑠 ∈ (2nd𝑦)
3128, 30, 20w3a 978 . . . . . . 7 wff (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
3231, 11, 22wrex 2456 . . . . . 6 wff 𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
3332, 5, 22wrex 2456 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
3433, 16, 22crab 2459 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
3525, 34cop 3594 . . 3 class ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩
362, 3, 4, 4, 35cmpo 5871 . 2 class (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
371, 36wceq 1353 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  7519  addnqpru  7520  addclpr  7527  plpvlu  7528  dmplp  7530  addnqprlemrl  7547  addnqprlemru  7548  addassprg  7569  distrlem1prl  7572  distrlem1pru  7573  distrlem4prl  7574  distrlem4pru  7575  distrlem5prl  7576  distrlem5pru  7577  ltaddpr  7587  ltexprlemfl  7599  ltexprlemrl  7600  ltexprlemfu  7601  ltexprlemru  7602  addcanprleml  7604  addcanprlemu  7605  cauappcvgprlemladdfu  7644  cauappcvgprlemladdfl  7645  caucvgprlemladdfu  7667
  Copyright terms: Public domain W3C validator