Definition df-mqqs 6448

Description: Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.4 of [Gleason] p. 119. (Contributed by NM, 24-Aug-1995.)

Assertion

Ref	Expression
df-mqqs	⊢ ·Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ ⟨𝑢, 𝑓⟩)] ~Q ))}

Distinct variable group:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑓

Detailed syntax breakdown of Definition df-mqqs

Step	Hyp	Ref	Expression
1		cmq 6381	. 2 class ·Q
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1242	. . . . . 6 class 𝑥
4		cnq 6378	. . . . . 6 class Q
5	3, 4	wcel 1393	. . . . 5 wff 𝑥 ∈ Q
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1242	. . . . . 6 class 𝑦
8	7, 4	wcel 1393	. . . . 5 wff 𝑦 ∈ Q
9	5, 8	wa 97	. . . 4 wff (𝑥 ∈ Q ∧ 𝑦 ∈ Q)
10		vw	. . . . . . . . . . . . . 14 setvar 𝑤
11	10	cv 1242	. . . . . . . . . . . . 13 class 𝑤
12		vv	. . . . . . . . . . . . . 14 setvar 𝑣
13	12	cv 1242	. . . . . . . . . . . . 13 class 𝑣
14	11, 13	cop 3378	. . . . . . . . . . . 12 class ⟨𝑤, 𝑣⟩
15		ceq 6377	. . . . . . . . . . . 12 class ~Q
16	14, 15	cec 6104	. . . . . . . . . . 11 class [⟨𝑤, 𝑣⟩] ~Q
17	3, 16	wceq 1243	. . . . . . . . . 10 wff 𝑥 = [⟨𝑤, 𝑣⟩] ~Q
18		vu	. . . . . . . . . . . . . 14 setvar 𝑢
19	18	cv 1242	. . . . . . . . . . . . 13 class 𝑢
20		vf	. . . . . . . . . . . . . 14 setvar 𝑓
21	20	cv 1242	. . . . . . . . . . . . 13 class 𝑓
22	19, 21	cop 3378	. . . . . . . . . . . 12 class ⟨𝑢, 𝑓⟩
23	22, 15	cec 6104	. . . . . . . . . . 11 class [⟨𝑢, 𝑓⟩] ~Q
24	7, 23	wceq 1243	. . . . . . . . . 10 wff 𝑦 = [⟨𝑢, 𝑓⟩] ~Q
25	17, 24	wa 97	. . . . . . . . 9 wff (𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q )
26		vz	. . . . . . . . . . 11 setvar 𝑧
27	26	cv 1242	. . . . . . . . . 10 class 𝑧
28		cmpq 6375	. . . . . . . . . . . 12 class ·pQ
29	14, 22, 28	co 5512	. . . . . . . . . . 11 class (⟨𝑤, 𝑣⟩ ·pQ ⟨𝑢, 𝑓⟩)
30	29, 15	cec 6104	. . . . . . . . . 10 class [(⟨𝑤, 𝑣⟩ ·pQ ⟨𝑢, 𝑓⟩)] ~Q
31	27, 30	wceq 1243	. . . . . . . . 9 wff 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ ⟨𝑢, 𝑓⟩)] ~Q
32	25, 31	wa 97	. . . . . . . 8 wff ((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ ⟨𝑢, 𝑓⟩)] ~Q )
33	32, 20	wex 1381	. . . . . . 7 wff ∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ ⟨𝑢, 𝑓⟩)] ~Q )
34	33, 18	wex 1381	. . . . . 6 wff ∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ ⟨𝑢, 𝑓⟩)] ~Q )
35	34, 12	wex 1381	. . . . 5 wff ∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ ⟨𝑢, 𝑓⟩)] ~Q )
36	35, 10	wex 1381	. . . 4 wff ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ ⟨𝑢, 𝑓⟩)] ~Q )
37	9, 36	wa 97	. . 3 wff ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ ⟨𝑢, 𝑓⟩)] ~Q ))
38	37, 2, 6, 26	coprab 5513	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ ⟨𝑢, 𝑓⟩)] ~Q ))}
39	1, 38	wceq 1243	1 wff ·Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ ⟨𝑢, 𝑓⟩)] ~Q ))}

This definition is referenced by:  mulpipqqs  6471  dmmulpq  6478