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

Definition df-imp 7245
Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7244 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 7070 . 2 class ·P
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cnp 7067 . . 3 class P
5 vr . . . . . . . . . 10 setvar 𝑟
65cv 1315 . . . . . . . . 9 class 𝑟
72cv 1315 . . . . . . . . . 10 class 𝑥
8 c1st 6004 . . . . . . . . . 10 class 1st
97, 8cfv 5093 . . . . . . . . 9 class (1st𝑥)
106, 9wcel 1465 . . . . . . . 8 wff 𝑟 ∈ (1st𝑥)
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1315 . . . . . . . . 9 class 𝑠
133cv 1315 . . . . . . . . . 10 class 𝑦
1413, 8cfv 5093 . . . . . . . . 9 class (1st𝑦)
1512, 14wcel 1465 . . . . . . . 8 wff 𝑠 ∈ (1st𝑦)
16 vq . . . . . . . . . 10 setvar 𝑞
1716cv 1315 . . . . . . . . 9 class 𝑞
18 cmq 7059 . . . . . . . . . 10 class ·Q
196, 12, 18co 5742 . . . . . . . . 9 class (𝑟 ·Q 𝑠)
2017, 19wceq 1316 . . . . . . . 8 wff 𝑞 = (𝑟 ·Q 𝑠)
2110, 15, 20w3a 947 . . . . . . 7 wff (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
22 cnq 7056 . . . . . . 7 class Q
2321, 11, 22wrex 2394 . . . . . 6 wff 𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
2423, 5, 22wrex 2394 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
2524, 16, 22crab 2397 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
26 c2nd 6005 . . . . . . . . . 10 class 2nd
277, 26cfv 5093 . . . . . . . . 9 class (2nd𝑥)
286, 27wcel 1465 . . . . . . . 8 wff 𝑟 ∈ (2nd𝑥)
2913, 26cfv 5093 . . . . . . . . 9 class (2nd𝑦)
3012, 29wcel 1465 . . . . . . . 8 wff 𝑠 ∈ (2nd𝑦)
3128, 30, 20w3a 947 . . . . . . 7 wff (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
3231, 11, 22wrex 2394 . . . . . 6 wff 𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
3332, 5, 22wrex 2394 . . . . 5 wff 𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
3433, 16, 22crab 2397 . . . 4 class {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
3525, 34cop 3500 . . 3 class ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩
362, 3, 4, 4, 35cmpo 5744 . 2 class (𝑥P, 𝑦P ↦ ⟨{𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (1st𝑥) ∧ 𝑠 ∈ (1st𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞Q ∣ ∃𝑟Q𝑠Q (𝑟 ∈ (2nd𝑥) ∧ 𝑠 ∈ (2nd𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
371, 36wceq 1316 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  7315  dmmp  7317  mulnqprl  7344  mulnqpru  7345  mulclpr  7348  mulnqprlemrl  7349  mulnqprlemru  7350  mulassprg  7357  distrlem1prl  7358  distrlem1pru  7359  distrlem4prl  7360  distrlem4pru  7361  distrlem5prl  7362  distrlem5pru  7363  1idprl  7366  1idpru  7367  recexprlem1ssl  7409  recexprlem1ssu  7410  recexprlemss1l  7411  recexprlemss1u  7412
  Copyright terms: Public domain W3C validator