Definition df-imp 7531

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7530 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

Step	Hyp	Ref	Expression
1		cmp 7356	. 2 class ·P
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cnp 7353	. . 3 class P
5		vr	. . . . . . . . . 10 setvar 𝑟
6	5	cv 1363	. . . . . . . . 9 class 𝑟
7	2	cv 1363	. . . . . . . . . 10 class 𝑥
8		c1st 6193	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5255	. . . . . . . . 9 class (1st ‘𝑥)
10	6, 9	wcel 2164	. . . . . . . 8 wff 𝑟 ∈ (1st ‘𝑥)
11		vs	. . . . . . . . . 10 setvar 𝑠
12	11	cv 1363	. . . . . . . . 9 class 𝑠
13	3	cv 1363	. . . . . . . . . 10 class 𝑦
14	13, 8	cfv 5255	. . . . . . . . 9 class (1st ‘𝑦)
15	12, 14	wcel 2164	. . . . . . . 8 wff 𝑠 ∈ (1st ‘𝑦)
16		vq	. . . . . . . . . 10 setvar 𝑞
17	16	cv 1363	. . . . . . . . 9 class 𝑞
18		cmq 7345	. . . . . . . . . 10 class ·Q
19	6, 12, 18	co 5919	. . . . . . . . 9 class (𝑟 ·Q 𝑠)
20	17, 19	wceq 1364	. . . . . . . 8 wff 𝑞 = (𝑟 ·Q 𝑠)
21	10, 15, 20	w3a 980	. . . . . . 7 wff (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
22		cnq 7342	. . . . . . 7 class Q
23	21, 11, 22	wrex 2473	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
24	23, 5, 22	wrex 2473	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
25	24, 16, 22	crab 2476	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
26		c2nd 6194	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5255	. . . . . . . . 9 class (2nd ‘𝑥)
28	6, 27	wcel 2164	. . . . . . . 8 wff 𝑟 ∈ (2nd ‘𝑥)
29	13, 26	cfv 5255	. . . . . . . . 9 class (2nd ‘𝑦)
30	12, 29	wcel 2164	. . . . . . . 8 wff 𝑠 ∈ (2nd ‘𝑦)
31	28, 30, 20	w3a 980	. . . . . . 7 wff (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
32	31, 11, 22	wrex 2473	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
33	32, 5, 22	wrex 2473	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
34	33, 16, 22	crab 2476	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
35	25, 34	cop 3622	. . 3 class ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩
36	2, 3, 4, 4, 35	cmpo 5921	. 2 class (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
37	1, 36	wceq 1364	1 wff ·P = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)

This definition is referenced by:  mpvlu  7601  dmmp  7603  mulnqprl  7630  mulnqpru  7631  mulclpr  7634  mulnqprlemrl  7635  mulnqprlemru  7636  mulassprg  7643  distrlem1prl  7644  distrlem1pru  7645  distrlem4prl  7646  distrlem4pru  7647  distrlem5prl  7648  distrlem5pru  7649  1idprl  7652  1idpru  7653  recexprlem1ssl  7695  recexprlem1ssu  7696  recexprlemss1l  7697  recexprlemss1u  7698