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

Definition df-imp 6565
Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 6564 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 6390 . 2 class ·P
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cnp 6387 . . 3 class P
5 vr . . . . . . . . . 10 setvar 𝑟
65cv 1242 . . . . . . . . 9 class 𝑟
72cv 1242 . . . . . . . . . 10 class 𝑥
8 c1st 5765 . . . . . . . . . 10 class 1st
97, 8cfv 4902 . . . . . . . . 9 class (1st𝑥)
106, 9wcel 1393 . . . . . . . 8 wff 𝑟 ∈ (1st𝑥)
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1242 . . . . . . . . 9 class 𝑠
133cv 1242 . . . . . . . . . 10 class 𝑦
1413, 8cfv 4902 . . . . . . . . 9 class (1st𝑦)
1512, 14wcel 1393 . . . . . . . 8 wff 𝑠 ∈ (1st𝑦)
16 vq . . . . . . . . . 10 setvar 𝑞
1716cv 1242 . . . . . . . . 9 class 𝑞
18 cmq 6379 . . . . . . . . . 10 class ·Q
196, 12, 18co 5512 . . . . . . . . 9 class (𝑟 ·Q 𝑠)
2017, 19wceq 1243 . . . . . . . 8 wff 𝑞 = (𝑟 ·Q 𝑠)
2110, 15, 20w3a 885 . . . . . . 7 wff (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
22 cnq 6376 . . . . . . 7 class Q
2321, 11, 22wrex 2307 . . . . . 6 wff 𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
2423, 5, 22wrex 2307 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
2524, 16, 22crab 2310 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
26 c2nd 5766 . . . . . . . . . 10 class 2nd
277, 26cfv 4902 . . . . . . . . 9 class (2nd𝑥)
286, 27wcel 1393 . . . . . . . 8 wff 𝑟 ∈ (2nd𝑥)
2913, 26cfv 4902 . . . . . . . . 9 class (2nd𝑦)
3012, 29wcel 1393 . . . . . . . 8 wff 𝑠 ∈ (2nd𝑦)
3128, 30, 20w3a 885 . . . . . . 7 wff (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
3231, 11, 22wrex 2307 . . . . . 6 wff 𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
3332, 5, 22wrex 2307 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
3433, 16, 22crab 2310 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
3525, 34cop 3378 . . 3 class ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩
362, 3, 4, 4, 35cmpt2 5514 . 2 class (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
371, 36wceq 1243 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  6635  dmmp  6637  mulnqprl  6664  mulnqpru  6665  mulclpr  6668  mulnqprlemrl  6669  mulnqprlemru  6670  mulassprg  6677  distrlem1prl  6678  distrlem1pru  6679  distrlem4prl  6680  distrlem4pru  6681  distrlem5prl  6682  distrlem5pru  6683  1idprl  6686  1idpru  6687  recexprlem1ssl  6729  recexprlem1ssu  6730  recexprlemss1l  6731  recexprlemss1u  6732
  Copyright terms: Public domain W3C validator