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

Definition df-iplp 6450
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 (for example, 𝑟 Q and 𝑟 (1stx)) conditions are redundant and can be simplified as shown at genpdf 6490.

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 = (x P, y P ↦ ⟨{𝑞 Q𝑟 Q 𝑠 Q (𝑟 (1stx) 𝑠 (1sty) 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 Q𝑟 Q 𝑠 Q (𝑟 (2ndx) 𝑠 (2ndy) 𝑞 = (𝑟 +Q 𝑠))}⟩)
Distinct variable group:   x,y,𝑞,𝑟,𝑠

Detailed syntax breakdown of Definition df-iplp
StepHypRef Expression
1 cpp 6277 . 2 class +P
2 vx . . 3 setvar x
3 vy . . 3 setvar y
4 cnp 6275 . . 3 class P
5 vr . . . . . . . . . 10 setvar 𝑟
65cv 1241 . . . . . . . . 9 class 𝑟
72cv 1241 . . . . . . . . . 10 class x
8 c1st 5707 . . . . . . . . . 10 class 1st
97, 8cfv 4845 . . . . . . . . 9 class (1stx)
106, 9wcel 1390 . . . . . . . 8 wff 𝑟 (1stx)
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1241 . . . . . . . . 9 class 𝑠
133cv 1241 . . . . . . . . . 10 class y
1413, 8cfv 4845 . . . . . . . . 9 class (1sty)
1512, 14wcel 1390 . . . . . . . 8 wff 𝑠 (1sty)
16 vq . . . . . . . . . 10 setvar 𝑞
1716cv 1241 . . . . . . . . 9 class 𝑞
18 cplq 6266 . . . . . . . . . 10 class +Q
196, 12, 18co 5455 . . . . . . . . 9 class (𝑟 +Q 𝑠)
2017, 19wceq 1242 . . . . . . . 8 wff 𝑞 = (𝑟 +Q 𝑠)
2110, 15, 20w3a 884 . . . . . . 7 wff (𝑟 (1stx) 𝑠 (1sty) 𝑞 = (𝑟 +Q 𝑠))
22 cnq 6264 . . . . . . 7 class Q
2321, 11, 22wrex 2301 . . . . . 6 wff 𝑠 Q (𝑟 (1stx) 𝑠 (1sty) 𝑞 = (𝑟 +Q 𝑠))
2423, 5, 22wrex 2301 . . . . 5 wff 𝑟 Q 𝑠 Q (𝑟 (1stx) 𝑠 (1sty) 𝑞 = (𝑟 +Q 𝑠))
2524, 16, 22crab 2304 . . . 4 class {𝑞 Q𝑟 Q 𝑠 Q (𝑟 (1stx) 𝑠 (1sty) 𝑞 = (𝑟 +Q 𝑠))}
26 c2nd 5708 . . . . . . . . . 10 class 2nd
277, 26cfv 4845 . . . . . . . . 9 class (2ndx)
286, 27wcel 1390 . . . . . . . 8 wff 𝑟 (2ndx)
2913, 26cfv 4845 . . . . . . . . 9 class (2ndy)
3012, 29wcel 1390 . . . . . . . 8 wff 𝑠 (2ndy)
3128, 30, 20w3a 884 . . . . . . 7 wff (𝑟 (2ndx) 𝑠 (2ndy) 𝑞 = (𝑟 +Q 𝑠))
3231, 11, 22wrex 2301 . . . . . 6 wff 𝑠 Q (𝑟 (2ndx) 𝑠 (2ndy) 𝑞 = (𝑟 +Q 𝑠))
3332, 5, 22wrex 2301 . . . . 5 wff 𝑟 Q 𝑠 Q (𝑟 (2ndx) 𝑠 (2ndy) 𝑞 = (𝑟 +Q 𝑠))
3433, 16, 22crab 2304 . . . 4 class {𝑞 Q𝑟 Q 𝑠 Q (𝑟 (2ndx) 𝑠 (2ndy) 𝑞 = (𝑟 +Q 𝑠))}
3525, 34cop 3370 . . 3 class ⟨{𝑞 Q𝑟 Q 𝑠 Q (𝑟 (1stx) 𝑠 (1sty) 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 Q𝑟 Q 𝑠 Q (𝑟 (2ndx) 𝑠 (2ndy) 𝑞 = (𝑟 +Q 𝑠))}⟩
362, 3, 4, 4, 35cmpt2 5457 . 2 class (x P, y P ↦ ⟨{𝑞 Q𝑟 Q 𝑠 Q (𝑟 (1stx) 𝑠 (1sty) 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 Q𝑟 Q 𝑠 Q (𝑟 (2ndx) 𝑠 (2ndy) 𝑞 = (𝑟 +Q 𝑠))}⟩)
371, 36wceq 1242 1 wff +P = (x P, y P ↦ ⟨{𝑞 Q𝑟 Q 𝑠 Q (𝑟 (1stx) 𝑠 (1sty) 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 Q𝑟 Q 𝑠 Q (𝑟 (2ndx) 𝑠 (2ndy) 𝑞 = (𝑟 +Q 𝑠))}⟩)
Colors of variables: wff set class
This definition is referenced by:  addnqprl  6511  addnqpru  6512  addclpr  6519  plpvlu  6520  dmplp  6522  addnqprlemrl  6537  addnqprlemru  6538  addassprg  6554  distrlem1prl  6557  distrlem1pru  6558  distrlem4prl  6559  distrlem4pru  6560  distrlem5prl  6561  distrlem5pru  6562  ltaddpr  6570  ltexprlemfl  6582  ltexprlemrl  6583  ltexprlemfu  6584  ltexprlemru  6585  addcanprleml  6587  addcanprlemu  6588  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626
  Copyright terms: Public domain W3C validator