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

Definition df-imp 6452
Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 6451 or the definition of multiplication on positive reals in Metamath Proof Explorer. This is as opposed to the more complicated definition of multiplication given in Section 11.2.1 of [HoTT], p. (varies), which appears to be motivated by handling negative numbers or handling modified Dedekind cuts in which locatedness is omitted.

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, 29-Sep-2019.)

Assertion
Ref Expression
df-imp ·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-imp
StepHypRef Expression
1 cmp 6278 . 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 cmq 6267 . . . . . . . . . 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:  mpvlu  6522  dmmp  6524  mulnqprl  6549  mulnqpru  6550  mulclpr  6553  mulassprg  6557  distrlem1prl  6558  distrlem1pru  6559  distrlem4prl  6560  distrlem4pru  6561  distrlem5prl  6562  distrlem5pru  6563  1idprl  6566  1idpru  6567  recexprlem1ssl  6605  recexprlem1ssu  6606  recexprlemss1l  6607  recexprlemss1u  6608
  Copyright terms: Public domain W3C validator