Definition df-mpq 3830

Description: Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 4034, and is intended to be used only by the construction. From Proposition 9-2.4 of [Gleason] p. 119.

Assertion

Ref	Expression
df-mpq	⊢ ·pQ = {⟨⟨x, y⟩, z⟩∣((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w ·N u), (v ·N f)⟩))}

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

Detailed syntax breakdown of Definition df-mpq

Step	Hyp	Ref	Expression
1		cmpq 3771	. 2 class ·pQ
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cnpi 3766	. . . . . . 7 class N
5	4, 4	cxp 2408	. . . . . 6 class (N × N)
6	3, 5	wcel 1092	. . . . 5 wff x ∈ (N × N)
7		vy	. . . . . . 7 set y
8	7	cv 1089	. . . . . 6 class y
9	8, 5	wcel 1092	. . . . 5 wff y ∈ (N × N)
10	6, 9	wa 196	. . . 4 wff (x ∈ (N × N) ∧ y ∈ (N × N))
11		vw	. . . . . . . . . . . . 13 set w
12	11	cv 1089	. . . . . . . . . . . 12 class w
13		vv	. . . . . . . . . . . . 13 set v
14	13	cv 1089	. . . . . . . . . . . 12 class v
15	12, 14	cop 1810	. . . . . . . . . . 11 class ⟨w, v⟩
16	3, 15	wceq 1091	. . . . . . . . . 10 wff x = ⟨w, v⟩
17		vu	. . . . . . . . . . . . 13 set u
18	17	cv 1089	. . . . . . . . . . . 12 class u
19		vf	. . . . . . . . . . . . 13 set f
20	19	cv 1089	. . . . . . . . . . . 12 class f
21	18, 20	cop 1810	. . . . . . . . . . 11 class ⟨u, f⟩
22	8, 21	wceq 1091	. . . . . . . . . 10 wff y = ⟨u, f⟩
23	16, 22	wa 196	. . . . . . . . 9 wff (x = ⟨w, v⟩ ∧ y = ⟨u, f⟩)
24		vz	. . . . . . . . . . 11 set z
25	24	cv 1089	. . . . . . . . . 10 class z
26		cmi 3768	. . . . . . . . . . . 12 class ·N
27	12, 18, 26	co 3001	. . . . . . . . . . 11 class (w ·N u)
28	14, 20, 26	co 3001	. . . . . . . . . . 11 class (v ·N f)
29	27, 28	cop 1810	. . . . . . . . . 10 class ⟨(w ·N u), (v ·N f)⟩
30	25, 29	wceq 1091	. . . . . . . . 9 wff z = ⟨(w ·N u), (v ·N f)⟩
31	23, 30	wa 196	. . . . . . . 8 wff ((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w ·N u), (v ·N f)⟩)
32	31, 19	wex 678	. . . . . . 7 wff ∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w ·N u), (v ·N f)⟩)
33	32, 17	wex 678	. . . . . 6 wff ∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w ·N u), (v ·N f)⟩)
34	33, 13	wex 678	. . . . 5 wff ∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w ·N u), (v ·N f)⟩)
35	34, 11	wex 678	. . . 4 wff ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w ·N u), (v ·N f)⟩)
36	10, 35	wa 196	. . 3 wff ((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w ·N u), (v ·N f)⟩))
37	36, 2, 7, 24	copab2 3002	. 2 class {⟨⟨x, y⟩, z⟩∣((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w ·N u), (v ·N f)⟩))}
38	1, 37	wceq 1091	1 wff ·pQ = {⟨⟨x, y⟩, z⟩∣((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w ·N u), (v ·N f)⟩))}

This definition is referenced by:  mulpipq 3849

metamath.org