Definition df-imp 7555

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7554 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 7380	. 2 class ·P
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cnp 7377	. . 3 class P
5		vr	. . . . . . . . . 10 setvar 𝑟
6	5	cv 1363	. . . . . . . . 9 class 𝑟
7	2	cv 1363	. . . . . . . . . 10 class 𝑥
8		c1st 6205	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5259	. . . . . . . . 9 class (1st ‘𝑥)
10	6, 9	wcel 2167	. . . . . . . 8 wff 𝑟 ∈ (1st ‘𝑥)
11		vs	. . . . . . . . . 10 setvar 𝑠
12	11	cv 1363	. . . . . . . . 9 class 𝑠
13	3	cv 1363	. . . . . . . . . 10 class 𝑦
14	13, 8	cfv 5259	. . . . . . . . 9 class (1st ‘𝑦)
15	12, 14	wcel 2167	. . . . . . . 8 wff 𝑠 ∈ (1st ‘𝑦)
16		vq	. . . . . . . . . 10 setvar 𝑞
17	16	cv 1363	. . . . . . . . 9 class 𝑞
18		cmq 7369	. . . . . . . . . 10 class ·Q
19	6, 12, 18	co 5925	. . . . . . . . 9 class (𝑟 ·Q 𝑠)
20	17, 19	wceq 1364	. . . . . . . 8 wff 𝑞 = (𝑟 ·Q 𝑠)
21	10, 15, 20	w3a 980	. . . . . . 7 wff (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
22		cnq 7366	. . . . . . 7 class Q
23	21, 11, 22	wrex 2476	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
24	23, 5, 22	wrex 2476	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
25	24, 16, 22	crab 2479	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
26		c2nd 6206	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5259	. . . . . . . . 9 class (2nd ‘𝑥)
28	6, 27	wcel 2167	. . . . . . . 8 wff 𝑟 ∈ (2nd ‘𝑥)
29	13, 26	cfv 5259	. . . . . . . . 9 class (2nd ‘𝑦)
30	12, 29	wcel 2167	. . . . . . . 8 wff 𝑠 ∈ (2nd ‘𝑦)
31	28, 30, 20	w3a 980	. . . . . . 7 wff (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
32	31, 11, 22	wrex 2476	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
33	32, 5, 22	wrex 2476	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))
34	33, 16, 22	crab 2479	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
35	25, 34	cop 3626	. . 3 class ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩
36	2, 3, 4, 4, 35	cmpo 5927	. 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  7625  dmmp  7627  mulnqprl  7654  mulnqpru  7655  mulclpr  7658  mulnqprlemrl  7659  mulnqprlemru  7660  mulassprg  7667  distrlem1prl  7668  distrlem1pru  7669  distrlem4prl  7670  distrlem4pru  7671  distrlem5prl  7672  distrlem5pru  7673  1idprl  7676  1idpru  7677  recexprlem1ssl  7719  recexprlem1ssu  7720  recexprlemss1l  7721  recexprlemss1u  7722