Definition df-imp 7843

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7842 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 7668	. 2 class ·P
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cnp 7665	. . 3 class P
5		vr	. . . . . . . . . 10 setvar 𝑟
6	5	cv 1401	. . . . . . . . 9 class 𝑟
7	2	cv 1401	. . . . . . . . . 10 class 𝑥
8		c1st 6376	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5380	. . . . . . . . 9 class (1st ‘𝑥)
10	6, 9	wcel 2209	. . . . . . . 8 wff 𝑟 ∈ (1st ‘𝑥)
11		vs	. . . . . . . . . 10 setvar 𝑠
12	11	cv 1401	. . . . . . . . 9 class 𝑠
13	3	cv 1401	. . . . . . . . . 10 class 𝑦
14	13, 8	cfv 5380	. . . . . . . . 9 class (1st ‘𝑦)
15	12, 14	wcel 2209	. . . . . . . 8 wff 𝑠 ∈ (1st ‘𝑦)
16		vq	. . . . . . . . . 10 setvar 𝑞
17	16	cv 1401	. . . . . . . . 9 class 𝑞
18		cmq 7657	. . . . . . . . . 10 class ·Q
19	6, 12, 18	co 6088	. . . . . . . . 9 class (𝑟 ·Q 𝑠)
20	17, 19	wceq 1402	. . . . . . . 8 wff 𝑞 = (𝑟 ·Q 𝑠)
21	10, 15, 20	w3a 1009	. . . . . . 7 wff (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
22		cnq 7654	. . . . . . 7 class Q
23	21, 11, 22	wrex 2529	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
24	23, 5, 22	wrex 2529	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
25	24, 16, 22	crab 2532	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
26		c2nd 6377	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5380	. . . . . . . . 9 class (2nd ‘𝑥)
28	6, 27	wcel 2209	. . . . . . . 8 wff 𝑟 ∈ (2nd ‘𝑥)
29	13, 26	cfv 5380	. . . . . . . . 9 class (2nd ‘𝑦)
30	12, 29	wcel 2209	. . . . . . . 8 wff 𝑠 ∈ (2nd ‘𝑦)
31	28, 30, 20	w3a 1009	. . . . . . 7 wff (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
32	31, 11, 22	wrex 2529	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
33	32, 5, 22	wrex 2529	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
34	33, 16, 22	crab 2532	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
35	25, 34	cop 3712	. . 3 class ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩
36	2, 3, 4, 4, 35	cmpo 6090	. 2 class (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
37	1, 36	wceq 1402	1 wff ·P = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)

This definition is used by:  mpvlu  7913  dmmp  7915  mulnqprl  7942  mulnqpru  7943  mulclpr  7946  mulnqprlemrl  7947  mulnqprlemru  7948  mulassprg  7955  distrlem1prl  7956  distrlem1pru  7957  distrlem4prl  7958  distrlem4pru  7959  distrlem5prl  7960  distrlem5pru  7961  1idprl  7964  1idpru  7965  recexprlem1ssl  8007  recexprlem1ssu  8008  recexprlemss1l  8009  recexprlemss1u  8010