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

Definition df-imp 6972
Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 6971 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 = (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
Distinct variable group:   𝑥,𝑦,𝑞,𝑟,𝑠

Detailed syntax breakdown of Definition df-imp
StepHypRef Expression
1 cmp 6797 . 2 class ·P
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cnp 6794 . . 3 class P
5 vr . . . . . . . . . 10 setvar 𝑟
65cv 1286 . . . . . . . . 9 class 𝑟
72cv 1286 . . . . . . . . . 10 class 𝑥
8 c1st 5866 . . . . . . . . . 10 class 1st
97, 8cfv 4981 . . . . . . . . 9 class (1st𝑥)
106, 9wcel 1436 . . . . . . . 8 wff 𝑟 ∈ (1st𝑥)
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1286 . . . . . . . . 9 class 𝑠
133cv 1286 . . . . . . . . . 10 class 𝑦
1413, 8cfv 4981 . . . . . . . . 9 class (1st𝑦)
1512, 14wcel 1436 . . . . . . . 8 wff 𝑠 ∈ (1st𝑦)
16 vq . . . . . . . . . 10 setvar 𝑞
1716cv 1286 . . . . . . . . 9 class 𝑞
18 cmq 6786 . . . . . . . . . 10 class ·Q
196, 12, 18co 5613 . . . . . . . . 9 class (𝑟 ·Q 𝑠)
2017, 19wceq 1287 . . . . . . . 8 wff 𝑞 = (𝑟 ·Q 𝑠)
2110, 15, 20w3a 922 . . . . . . 7 wff (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
22 cnq 6783 . . . . . . 7 class Q
2321, 11, 22wrex 2356 . . . . . 6 wff 𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
2423, 5, 22wrex 2356 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
2524, 16, 22crab 2359 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
26 c2nd 5867 . . . . . . . . . 10 class 2nd
277, 26cfv 4981 . . . . . . . . 9 class (2nd𝑥)
286, 27wcel 1436 . . . . . . . 8 wff 𝑟 ∈ (2nd𝑥)
2913, 26cfv 4981 . . . . . . . . 9 class (2nd𝑦)
3012, 29wcel 1436 . . . . . . . 8 wff 𝑠 ∈ (2nd𝑦)
3128, 30, 20w3a 922 . . . . . . 7 wff (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
3231, 11, 22wrex 2356 . . . . . 6 wff 𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
3332, 5, 22wrex 2356 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
3433, 16, 22crab 2359 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
3525, 34cop 3434 . . 3 class ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩
362, 3, 4, 4, 35cmpt2 5615 . 2 class (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
371, 36wceq 1287 1 wff ·P = (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
Colors of variables: wff set class
This definition is referenced by:  mpvlu  7042  dmmp  7044  mulnqprl  7071  mulnqpru  7072  mulclpr  7075  mulnqprlemrl  7076  mulnqprlemru  7077  mulassprg  7084  distrlem1prl  7085  distrlem1pru  7086  distrlem4prl  7087  distrlem4pru  7088  distrlem5prl  7089  distrlem5pru  7090  1idprl  7093  1idpru  7094  recexprlem1ssl  7136  recexprlem1ssu  7137  recexprlemss1l  7138  recexprlemss1u  7139
  Copyright terms: Public domain W3C validator