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

Definition df-imp 7241
Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7240 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 7066 . 2 class ·P
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cnp 7063 . . 3 class P
5 vr . . . . . . . . . 10 setvar 𝑟
65cv 1313 . . . . . . . . 9 class 𝑟
72cv 1313 . . . . . . . . . 10 class 𝑥
8 c1st 6002 . . . . . . . . . 10 class 1st
97, 8cfv 5091 . . . . . . . . 9 class (1st𝑥)
106, 9wcel 1463 . . . . . . . 8 wff 𝑟 ∈ (1st𝑥)
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1313 . . . . . . . . 9 class 𝑠
133cv 1313 . . . . . . . . . 10 class 𝑦
1413, 8cfv 5091 . . . . . . . . 9 class (1st𝑦)
1512, 14wcel 1463 . . . . . . . 8 wff 𝑠 ∈ (1st𝑦)
16 vq . . . . . . . . . 10 setvar 𝑞
1716cv 1313 . . . . . . . . 9 class 𝑞
18 cmq 7055 . . . . . . . . . 10 class ·Q
196, 12, 18co 5740 . . . . . . . . 9 class (𝑟 ·Q 𝑠)
2017, 19wceq 1314 . . . . . . . 8 wff 𝑞 = (𝑟 ·Q 𝑠)
2110, 15, 20w3a 945 . . . . . . 7 wff (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
22 cnq 7052 . . . . . . 7 class Q
2321, 11, 22wrex 2392 . . . . . 6 wff 𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
2423, 5, 22wrex 2392 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
2524, 16, 22crab 2395 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
26 c2nd 6003 . . . . . . . . . 10 class 2nd
277, 26cfv 5091 . . . . . . . . 9 class (2nd𝑥)
286, 27wcel 1463 . . . . . . . 8 wff 𝑟 ∈ (2nd𝑥)
2913, 26cfv 5091 . . . . . . . . 9 class (2nd𝑦)
3012, 29wcel 1463 . . . . . . . 8 wff 𝑠 ∈ (2nd𝑦)
3128, 30, 20w3a 945 . . . . . . 7 wff (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
3231, 11, 22wrex 2392 . . . . . 6 wff 𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
3332, 5, 22wrex 2392 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
3433, 16, 22crab 2395 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
3525, 34cop 3498 . . 3 class ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩
362, 3, 4, 4, 35cmpo 5742 . 2 class (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
371, 36wceq 1314 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  7311  dmmp  7313  mulnqprl  7340  mulnqpru  7341  mulclpr  7344  mulnqprlemrl  7345  mulnqprlemru  7346  mulassprg  7353  distrlem1prl  7354  distrlem1pru  7355  distrlem4prl  7356  distrlem4pru  7357  distrlem5prl  7358  distrlem5pru  7359  1idprl  7362  1idpru  7363  recexprlem1ssl  7405  recexprlem1ssu  7406  recexprlemss1l  7407  recexprlemss1u  7408
  Copyright terms: Public domain W3C validator