Definition df-mqqs 6327

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 = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ Q ∧ y ∈ Q) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~Q ∧ y = [⟨u, f⟩] ~Q ) ∧ z = [(⟨w, v⟩ ·pQ ⟨u, f⟩)] ~Q ))}

Distinct variable group:   x,y,z,w,v,u,f

Detailed syntax breakdown of Definition df-mqqs

Step	Hyp	Ref	Expression
1		cmq 6260	. 2 class ·Q
2		vx	. . . . . . 7 setvar x
3	2	cv 1241	. . . . . 6 class x
4		cnq 6257	. . . . . 6 class Q
5	3, 4	wcel 1390	. . . . 5 wff x ∈ Q
6		vy	. . . . . . 7 setvar y
7	6	cv 1241	. . . . . 6 class y
8	7, 4	wcel 1390	. . . . 5 wff y ∈ Q
9	5, 8	wa 97	. . . 4 wff (x ∈ Q ∧ y ∈ Q)
10		vw	. . . . . . . . . . . . . 14 setvar w
11	10	cv 1241	. . . . . . . . . . . . 13 class w
12		vv	. . . . . . . . . . . . . 14 setvar v
13	12	cv 1241	. . . . . . . . . . . . 13 class v
14	11, 13	cop 3369	. . . . . . . . . . . 12 class ⟨w, v⟩
15		ceq 6256	. . . . . . . . . . . 12 class ~Q
16	14, 15	cec 6033	. . . . . . . . . . 11 class [⟨w, v⟩] ~Q
17	3, 16	wceq 1242	. . . . . . . . . 10 wff x = [⟨w, v⟩] ~Q
18		vu	. . . . . . . . . . . . . 14 setvar u
19	18	cv 1241	. . . . . . . . . . . . 13 class u
20		vf	. . . . . . . . . . . . . 14 setvar f
21	20	cv 1241	. . . . . . . . . . . . 13 class f
22	19, 21	cop 3369	. . . . . . . . . . . 12 class ⟨u, f⟩
23	22, 15	cec 6033	. . . . . . . . . . 11 class [⟨u, f⟩] ~Q
24	7, 23	wceq 1242	. . . . . . . . . 10 wff y = [⟨u, f⟩] ~Q
25	17, 24	wa 97	. . . . . . . . 9 wff (x = [⟨w, v⟩] ~Q ∧ y = [⟨u, f⟩] ~Q )
26		vz	. . . . . . . . . . 11 setvar z
27	26	cv 1241	. . . . . . . . . 10 class z
28		cmpq 6254	. . . . . . . . . . . 12 class ·pQ
29	14, 22, 28	co 5452	. . . . . . . . . . 11 class (⟨w, v⟩ ·pQ ⟨u, f⟩)
30	29, 15	cec 6033	. . . . . . . . . 10 class [(⟨w, v⟩ ·pQ ⟨u, f⟩)] ~Q
31	27, 30	wceq 1242	. . . . . . . . 9 wff z = [(⟨w, v⟩ ·pQ ⟨u, f⟩)] ~Q
32	25, 31	wa 97	. . . . . . . 8 wff ((x = [⟨w, v⟩] ~Q ∧ y = [⟨u, f⟩] ~Q ) ∧ z = [(⟨w, v⟩ ·pQ ⟨u, f⟩)] ~Q )
33	32, 20	wex 1378	. . . . . . 7 wff ∃f((x = [⟨w, v⟩] ~Q ∧ y = [⟨u, f⟩] ~Q ) ∧ z = [(⟨w, v⟩ ·pQ ⟨u, f⟩)] ~Q )
34	33, 18	wex 1378	. . . . . 6 wff ∃u∃f((x = [⟨w, v⟩] ~Q ∧ y = [⟨u, f⟩] ~Q ) ∧ z = [(⟨w, v⟩ ·pQ ⟨u, f⟩)] ~Q )
35	34, 12	wex 1378	. . . . 5 wff ∃v∃u∃f((x = [⟨w, v⟩] ~Q ∧ y = [⟨u, f⟩] ~Q ) ∧ z = [(⟨w, v⟩ ·pQ ⟨u, f⟩)] ~Q )
36	35, 10	wex 1378	. . . 4 wff ∃w∃v∃u∃f((x = [⟨w, v⟩] ~Q ∧ y = [⟨u, f⟩] ~Q ) ∧ z = [(⟨w, v⟩ ·pQ ⟨u, f⟩)] ~Q )
37	9, 36	wa 97	. . 3 wff ((x ∈ Q ∧ y ∈ Q) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~Q ∧ y = [⟨u, f⟩] ~Q ) ∧ z = [(⟨w, v⟩ ·pQ ⟨u, f⟩)] ~Q ))
38	37, 2, 6, 26	coprab 5453	. 2 class {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ Q ∧ y ∈ Q) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~Q ∧ y = [⟨u, f⟩] ~Q ) ∧ z = [(⟨w, v⟩ ·pQ ⟨u, f⟩)] ~Q ))}
39	1, 38	wceq 1242	1 wff ·Q = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ Q ∧ y ∈ Q) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~Q ∧ y = [⟨u, f⟩] ~Q ) ∧ z = [(⟨w, v⟩ ·pQ ⟨u, f⟩)] ~Q ))}

This definition is referenced by:  mulpipqqs  6350  dmmulpq  6357