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

Definition df-iplp 6538
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 6578.

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 6363 . 2 class +P
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cnp 6361 . . 3 class P
5 vr . . . . . . . . . 10 setvar 𝑟
65cv 1242 . . . . . . . . 9 class 𝑟
72cv 1242 . . . . . . . . . 10 class 𝑥
8 c1st 5743 . . . . . . . . . 10 class 1st
97, 8cfv 4880 . . . . . . . . 9 class (1st𝑥)
106, 9wcel 1393 . . . . . . . 8 wff 𝑟 ∈ (1st𝑥)
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1242 . . . . . . . . 9 class 𝑠
133cv 1242 . . . . . . . . . 10 class 𝑦
1413, 8cfv 4880 . . . . . . . . 9 class (1st𝑦)
1512, 14wcel 1393 . . . . . . . 8 wff 𝑠 ∈ (1st𝑦)
16 vq . . . . . . . . . 10 setvar 𝑞
1716cv 1242 . . . . . . . . 9 class 𝑞
18 cplq 6352 . . . . . . . . . 10 class +Q
196, 12, 18co 5490 . . . . . . . . 9 class (𝑟 +Q 𝑠)
2017, 19wceq 1243 . . . . . . . 8 wff 𝑞 = (𝑟 +Q 𝑠)
2110, 15, 20w3a 885 . . . . . . 7 wff (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
22 cnq 6350 . . . . . . 7 class Q
2321, 11, 22wrex 2304 . . . . . 6 wff 𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
2423, 5, 22wrex 2304 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
2524, 16, 22crab 2307 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
26 c2nd 5744 . . . . . . . . . 10 class 2nd
277, 26cfv 4880 . . . . . . . . 9 class (2nd𝑥)
286, 27wcel 1393 . . . . . . . 8 wff 𝑟 ∈ (2nd𝑥)
2913, 26cfv 4880 . . . . . . . . 9 class (2nd𝑦)
3012, 29wcel 1393 . . . . . . . 8 wff 𝑠 ∈ (2nd𝑦)
3128, 30, 20w3a 885 . . . . . . 7 wff (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
3231, 11, 22wrex 2304 . . . . . 6 wff 𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
3332, 5, 22wrex 2304 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
3433, 16, 22crab 2307 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
3525, 34cop 3375 . . 3 class ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩
362, 3, 4, 4, 35cmpt2 5492 . 2 class (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
371, 36wceq 1243 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  6599  addnqpru  6600  addclpr  6607  plpvlu  6608  dmplp  6610  addnqprlemrl  6627  addnqprlemru  6628  addassprg  6649  distrlem1prl  6652  distrlem1pru  6653  distrlem4prl  6654  distrlem4pru  6655  distrlem5prl  6656  distrlem5pru  6657  ltaddpr  6667  ltexprlemfl  6679  ltexprlemrl  6680  ltexprlemfu  6681  ltexprlemru  6682  addcanprleml  6684  addcanprlemu  6685  cauappcvgprlemladdfu  6724  cauappcvgprlemladdfl  6725  caucvgprlemladdfu  6747
  Copyright terms: Public domain W3C validator