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

Definition df-imp 6567
 Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 6566 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 6392 . 2 class ·P
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cnp 6389 . . 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 6381 . . . . . . . . . 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 6378 . . . . . . 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  6637  dmmp  6639  mulnqprl  6666  mulnqpru  6667  mulclpr  6670  mulnqprlemrl  6671  mulnqprlemru  6672  mulassprg  6679  distrlem1prl  6680  distrlem1pru  6681  distrlem4prl  6682  distrlem4pru  6683  distrlem5prl  6684  distrlem5pru  6685  1idprl  6688  1idpru  6689  recexprlem1ssl  6731  recexprlem1ssu  6732  recexprlemss1l  6733  recexprlemss1u  6734
 Copyright terms: Public domain W3C validator