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

Definition df-iplp 7442
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 7482.

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 7267 . 2 class +P
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cnp 7265 . . 3 class P
5 vr . . . . . . . . . 10 setvar 𝑟
65cv 1352 . . . . . . . . 9 class 𝑟
72cv 1352 . . . . . . . . . 10 class 𝑥
8 c1st 6129 . . . . . . . . . 10 class 1st
97, 8cfv 5208 . . . . . . . . 9 class (1st𝑥)
106, 9wcel 2146 . . . . . . . 8 wff 𝑟 ∈ (1st𝑥)
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1352 . . . . . . . . 9 class 𝑠
133cv 1352 . . . . . . . . . 10 class 𝑦
1413, 8cfv 5208 . . . . . . . . 9 class (1st𝑦)
1512, 14wcel 2146 . . . . . . . 8 wff 𝑠 ∈ (1st𝑦)
16 vq . . . . . . . . . 10 setvar 𝑞
1716cv 1352 . . . . . . . . 9 class 𝑞
18 cplq 7256 . . . . . . . . . 10 class +Q
196, 12, 18co 5865 . . . . . . . . 9 class (𝑟 +Q 𝑠)
2017, 19wceq 1353 . . . . . . . 8 wff 𝑞 = (𝑟 +Q 𝑠)
2110, 15, 20w3a 978 . . . . . . 7 wff (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
22 cnq 7254 . . . . . . 7 class Q
2321, 11, 22wrex 2454 . . . . . 6 wff 𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
2423, 5, 22wrex 2454 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
2524, 16, 22crab 2457 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
26 c2nd 6130 . . . . . . . . . 10 class 2nd
277, 26cfv 5208 . . . . . . . . 9 class (2nd𝑥)
286, 27wcel 2146 . . . . . . . 8 wff 𝑟 ∈ (2nd𝑥)
2913, 26cfv 5208 . . . . . . . . 9 class (2nd𝑦)
3012, 29wcel 2146 . . . . . . . 8 wff 𝑠 ∈ (2nd𝑦)
3128, 30, 20w3a 978 . . . . . . 7 wff (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
3231, 11, 22wrex 2454 . . . . . 6 wff 𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
3332, 5, 22wrex 2454 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
3433, 16, 22crab 2457 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
3525, 34cop 3592 . . 3 class ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩
362, 3, 4, 4, 35cmpo 5867 . 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  7503  addnqpru  7504  addclpr  7511  plpvlu  7512  dmplp  7514  addnqprlemrl  7531  addnqprlemru  7532  addassprg  7553  distrlem1prl  7556  distrlem1pru  7557  distrlem4prl  7558  distrlem4pru  7559  distrlem5prl  7560  distrlem5pru  7561  ltaddpr  7571  ltexprlemfl  7583  ltexprlemrl  7584  ltexprlemfu  7585  ltexprlemru  7586  addcanprleml  7588  addcanprlemu  7589  cauappcvgprlemladdfu  7628  cauappcvgprlemladdfl  7629  caucvgprlemladdfu  7651
  Copyright terms: Public domain W3C validator