Definition df-imp 6451

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 6450 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  6521  dmmp  6523  mulnqprl  6548  mulnqpru  6549  mulclpr  6552  mulassprg  6556  distrlem1prl  6557  distrlem1pru  6558  distrlem4prl  6559  distrlem4pru  6560  distrlem5prl  6561  distrlem5pru  6562  1idprl  6565  1idpru  6566  recexprlem1ssl  6604  recexprlem1ssu  6605  recexprlemss1l  6606  recexprlemss1u  6607