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

Definition df-iplp 6451
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, 𝑟 (1stx) implies 𝑟 Q) and can be simplified as shown at genpdf 6491.

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  6512  addnqpru  6513  addclpr  6520  plpvlu  6521  dmplp  6523  addnqprlemrl  6538  addnqprlemru  6539  addassprg  6555  distrlem1prl  6558  distrlem1pru  6559  distrlem4prl  6560  distrlem4pru  6561  distrlem5prl  6562  distrlem5pru  6563  ltaddpr  6571  ltexprlemfl  6583  ltexprlemrl  6584  ltexprlemfu  6585  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  caucvgprlemladdfu  6648
  Copyright terms: Public domain W3C validator