Definition df-mq 3834

Description: Define 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-mq	|- .Q = {<.<.x, y>., z>. | ((x e. Q. /\ y e. Q.) /\ E.wE.vE.uE.f((x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q ) /\ z = [(<.w, v>. .pQ <.u, f>.)] ~Q ))}

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

Detailed syntax breakdown of Definition df-mq

Step	Hyp	Ref	Expression
1		cmq 3776	. 2 class .Q
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cnq 3773	. . . . . 6 class Q.
5	3, 4	wcel 1092	. . . . 5 wff x e. Q.
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wcel 1092	. . . . 5 wff y e. Q.
9	5, 8	wa 196	. . . 4 wff (x e. Q. /\ y e. Q.)
10		vw	. . . . . . . . . . . . . 14 set w
11	10	cv 1089	. . . . . . . . . . . . 13 class w
12		vv	. . . . . . . . . . . . . 14 set v
13	12	cv 1089	. . . . . . . . . . . . 13 class v
14	11, 13	cop 1810	. . . . . . . . . . . 12 class <.w, v>.
15		ceq 3772	. . . . . . . . . . . 12 class ~Q
16	14, 15	cec 3198	. . . . . . . . . . 11 class [<.w, v>.] ~Q
17	3, 16	wceq 1091	. . . . . . . . . 10 wff x = [<.w, v>.] ~Q
18		vu	. . . . . . . . . . . . . 14 set u
19	18	cv 1089	. . . . . . . . . . . . 13 class u
20		vf	. . . . . . . . . . . . . 14 set f
21	20	cv 1089	. . . . . . . . . . . . 13 class f
22	19, 21	cop 1810	. . . . . . . . . . . 12 class <.u, f>.
23	22, 15	cec 3198	. . . . . . . . . . 11 class [<.u, f>.] ~Q
24	7, 23	wceq 1091	. . . . . . . . . 10 wff y = [<.u, f>.] ~Q
25	17, 24	wa 196	. . . . . . . . 9 wff (x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q )
26		vz	. . . . . . . . . . 11 set z
27	26	cv 1089	. . . . . . . . . 10 class z
28		cmpq 3771	. . . . . . . . . . . 12 class .pQ
29	14, 22, 28	co 3001	. . . . . . . . . . 11 class (<.w, v>. .pQ <.u, f>.)
30	29, 15	cec 3198	. . . . . . . . . 10 class [(<.w, v>. .pQ <.u, f>.)] ~Q
31	27, 30	wceq 1091	. . . . . . . . 9 wff z = [(<.w, v>. .pQ <.u, f>.)] ~Q
32	25, 31	wa 196	. . . . . . . 8 wff ((x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q ) /\ z = [(<.w, v>. .pQ <.u, f>.)] ~Q )
33	32, 20	wex 678	. . . . . . 7 wff E.f((x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q ) /\ z = [(<.w, v>. .pQ <.u, f>.)] ~Q )
34	33, 18	wex 678	. . . . . 6 wff E.uE.f((x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q ) /\ z = [(<.w, v>. .pQ <.u, f>.)] ~Q )
35	34, 12	wex 678	. . . . 5 wff E.vE.uE.f((x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q ) /\ z = [(<.w, v>. .pQ <.u, f>.)] ~Q )
36	35, 10	wex 678	. . . 4 wff E.wE.vE.uE.f((x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q ) /\ z = [(<.w, v>. .pQ <.u, f>.)] ~Q )
37	9, 36	wa 196	. . 3 wff ((x e. Q. /\ y e. Q.) /\ E.wE.vE.uE.f((x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q ) /\ z = [(<.w, v>. .pQ <.u, f>.)] ~Q ))
38	37, 2, 6, 26	copab2 3002	. 2 class {<.<.x, y>., z>. | ((x e. Q. /\ y e. Q.) /\ E.wE.vE.uE.f((x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q ) /\ z = [(<.w, v>. .pQ <.u, f>.)] ~Q ))}
39	1, 38	wceq 1091	1 wff .Q = {<.<.x, y>., z>. | ((x e. Q. /\ y e. Q.) /\ E.wE.vE.uE.f((x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q ) /\ z = [(<.w, v>. .pQ <.u, f>.)] ~Q ))}

This definition is referenced by:  mulpipq 3849  dmmulpq 3855

metamath.org