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

Definition df-iplp 7124
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 7164.

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 6949 . 2 class +P
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cnp 6947 . . 3 class P
5 vr . . . . . . . . . 10 setvar 𝑟
65cv 1295 . . . . . . . . 9 class 𝑟
72cv 1295 . . . . . . . . . 10 class 𝑥
8 c1st 5947 . . . . . . . . . 10 class 1st
97, 8cfv 5049 . . . . . . . . 9 class (1st𝑥)
106, 9wcel 1445 . . . . . . . 8 wff 𝑟 ∈ (1st𝑥)
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1295 . . . . . . . . 9 class 𝑠
133cv 1295 . . . . . . . . . 10 class 𝑦
1413, 8cfv 5049 . . . . . . . . 9 class (1st𝑦)
1512, 14wcel 1445 . . . . . . . 8 wff 𝑠 ∈ (1st𝑦)
16 vq . . . . . . . . . 10 setvar 𝑞
1716cv 1295 . . . . . . . . 9 class 𝑞
18 cplq 6938 . . . . . . . . . 10 class +Q
196, 12, 18co 5690 . . . . . . . . 9 class (𝑟 +Q 𝑠)
2017, 19wceq 1296 . . . . . . . 8 wff 𝑞 = (𝑟 +Q 𝑠)
2110, 15, 20w3a 927 . . . . . . 7 wff (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
22 cnq 6936 . . . . . . 7 class Q
2321, 11, 22wrex 2371 . . . . . 6 wff 𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
2423, 5, 22wrex 2371 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
2524, 16, 22crab 2374 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
26 c2nd 5948 . . . . . . . . . 10 class 2nd
277, 26cfv 5049 . . . . . . . . 9 class (2nd𝑥)
286, 27wcel 1445 . . . . . . . 8 wff 𝑟 ∈ (2nd𝑥)
2913, 26cfv 5049 . . . . . . . . 9 class (2nd𝑦)
3012, 29wcel 1445 . . . . . . . 8 wff 𝑠 ∈ (2nd𝑦)
3128, 30, 20w3a 927 . . . . . . 7 wff (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
3231, 11, 22wrex 2371 . . . . . 6 wff 𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
3332, 5, 22wrex 2371 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))
3433, 16, 22crab 2374 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}
3525, 34cop 3469 . . 3 class ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩
362, 3, 4, 4, 35cmpt2 5692 . 2 class (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
371, 36wceq 1296 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  7185  addnqpru  7186  addclpr  7193  plpvlu  7194  dmplp  7196  addnqprlemrl  7213  addnqprlemru  7214  addassprg  7235  distrlem1prl  7238  distrlem1pru  7239  distrlem4prl  7240  distrlem4pru  7241  distrlem5prl  7242  distrlem5pru  7243  ltaddpr  7253  ltexprlemfl  7265  ltexprlemrl  7266  ltexprlemfu  7267  ltexprlemru  7268  addcanprleml  7270  addcanprlemu  7271  cauappcvgprlemladdfu  7310  cauappcvgprlemladdfl  7311  caucvgprlemladdfu  7333
  Copyright terms: Public domain W3C validator