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

Definition df-iplp 6443
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 6483.

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 6270 . 2 class +P
2 vx . . 3 setvar x
3 vy . . 3 setvar y
4 cnp 6268 . . 3 class P
5 vr . . . . . . . . . 10 setvar 𝑟
65cv 1241 . . . . . . . . 9 class 𝑟
72cv 1241 . . . . . . . . . 10 class x
8 c1st 5704 . . . . . . . . . 10 class 1st
97, 8cfv 4844 . . . . . . . . 9 class (1stx)
106, 9wcel 1390 . . . . . . . 8 wff 𝑟 (1stx)
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1241 . . . . . . . . 9 class 𝑠
133cv 1241 . . . . . . . . . 10 class y
1413, 8cfv 4844 . . . . . . . . 9 class (1sty)
1512, 14wcel 1390 . . . . . . . 8 wff 𝑠 (1sty)
16 vq . . . . . . . . . 10 setvar 𝑞
1716cv 1241 . . . . . . . . 9 class 𝑞
18 cplq 6259 . . . . . . . . . 10 class +Q
196, 12, 18co 5452 . . . . . . . . 9 class (𝑟 +Q 𝑠)
2017, 19wceq 1242 . . . . . . . 8 wff 𝑞 = (𝑟 +Q 𝑠)
2110, 15, 20w3a 884 . . . . . . 7 wff (𝑟 (1stx) 𝑠 (1sty) 𝑞 = (𝑟 +Q 𝑠))
22 cnq 6257 . . . . . . 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 5705 . . . . . . . . . 10 class 2nd
277, 26cfv 4844 . . . . . . . . 9 class (2ndx)
286, 27wcel 1390 . . . . . . . 8 wff 𝑟 (2ndx)
2913, 26cfv 4844 . . . . . . . . 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 3369 . . 3 class ⟨{𝑞 Q𝑟 Q 𝑠 Q (𝑟 (1stx) 𝑠 (1sty) 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 Q𝑟 Q 𝑠 Q (𝑟 (2ndx) 𝑠 (2ndy) 𝑞 = (𝑟 +Q 𝑠))}⟩
362, 3, 4, 4, 35cmpt2 5454 . 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  6505  addnqpru  6506  addclpr  6513  plpvlu  6514  dmplp  6516  addnqpr1lemrl  6529  addnqpr1lemru  6530  addassprg  6545  distrlem1prl  6548  distrlem1pru  6549  distrlem4prl  6550  distrlem4pru  6551  distrlem5prl  6552  distrlem5pru  6553  ltaddpr  6561  ltexprlemfl  6573  ltexprlemrl  6574  ltexprlemfu  6575  ltexprlemru  6576  addcanprleml  6578  addcanprlemu  6579
  Copyright terms: Public domain W3C validator