Definition df-imp 6452

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 6451 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 = (x ∈ P, y ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘x) ∧ 𝑠 ∈ (1st ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘x) ∧ 𝑠 ∈ (2nd ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)

Distinct variable group:   x,y,𝑞,𝑟,𝑠

Detailed syntax breakdown of Definition df-imp

Step	Hyp	Ref	Expression
1		cmp 6278	. 2 class ·P
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 6275	. . 3 class P
5		vr	. . . . . . . . . 10 setvar 𝑟
6	5	cv 1241	. . . . . . . . 9 class 𝑟
7	2	cv 1241	. . . . . . . . . 10 class x
8		c1st 5707	. . . . . . . . . 10 class 1st
9	7, 8	cfv 4845	. . . . . . . . 9 class (1st ‘x)
10	6, 9	wcel 1390	. . . . . . . 8 wff 𝑟 ∈ (1st ‘x)
11		vs	. . . . . . . . . 10 setvar 𝑠
12	11	cv 1241	. . . . . . . . 9 class 𝑠
13	3	cv 1241	. . . . . . . . . 10 class y
14	13, 8	cfv 4845	. . . . . . . . 9 class (1st ‘y)
15	12, 14	wcel 1390	. . . . . . . 8 wff 𝑠 ∈ (1st ‘y)
16		vq	. . . . . . . . . 10 setvar 𝑞
17	16	cv 1241	. . . . . . . . 9 class 𝑞
18		cmq 6267	. . . . . . . . . 10 class ·Q
19	6, 12, 18	co 5455	. . . . . . . . 9 class (𝑟 ·Q 𝑠)
20	17, 19	wceq 1242	. . . . . . . 8 wff 𝑞 = (𝑟 ·Q 𝑠)
21	10, 15, 20	w3a 884	. . . . . . 7 wff (𝑟 ∈ (1st ‘x) ∧ 𝑠 ∈ (1st ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))
22		cnq 6264	. . . . . . 7 class Q
23	21, 11, 22	wrex 2301	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘x) ∧ 𝑠 ∈ (1st ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))
24	23, 5, 22	wrex 2301	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘x) ∧ 𝑠 ∈ (1st ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))
25	24, 16, 22	crab 2304	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘x) ∧ 𝑠 ∈ (1st ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
26		c2nd 5708	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 4845	. . . . . . . . 9 class (2nd ‘x)
28	6, 27	wcel 1390	. . . . . . . 8 wff 𝑟 ∈ (2nd ‘x)
29	13, 26	cfv 4845	. . . . . . . . 9 class (2nd ‘y)
30	12, 29	wcel 1390	. . . . . . . 8 wff 𝑠 ∈ (2nd ‘y)
31	28, 30, 20	w3a 884	. . . . . . 7 wff (𝑟 ∈ (2nd ‘x) ∧ 𝑠 ∈ (2nd ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))
32	31, 11, 22	wrex 2301	. . . . . 6 wff ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘x) ∧ 𝑠 ∈ (2nd ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))
33	32, 5, 22	wrex 2301	. . . . 5 wff ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘x) ∧ 𝑠 ∈ (2nd ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))
34	33, 16, 22	crab 2304	. . . 4 class {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘x) ∧ 𝑠 ∈ (2nd ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}
35	25, 34	cop 3370	. . 3 class ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘x) ∧ 𝑠 ∈ (1st ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘x) ∧ 𝑠 ∈ (2nd ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩
36	2, 3, 4, 4, 35	cmpt2 5457	. 2 class (x ∈ P, y ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘x) ∧ 𝑠 ∈ (1st ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘x) ∧ 𝑠 ∈ (2nd ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
37	1, 36	wceq 1242	1 wff ·P = (x ∈ P, y ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘x) ∧ 𝑠 ∈ (1st ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘x) ∧ 𝑠 ∈ (2nd ‘y) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)

This definition is referenced by:  mpvlu  6522  dmmp  6524  mulnqprl  6549  mulnqpru  6550  mulclpr  6553  mulassprg  6557  distrlem1prl  6558  distrlem1pru  6559  distrlem4prl  6560  distrlem4pru  6561  distrlem5prl  6562  distrlem5pru  6563  1idprl  6566  1idpru  6567  recexprlem1ssl  6605  recexprlem1ssu  6606  recexprlemss1l  6607  recexprlemss1u  6608