Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-iplp 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, 𝑟 ∈ (1st ‘x) 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 𝑠))}⟩)