Definition df-plq 5026

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

Assertion

Ref	Expression
df-plq	|- +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:   x,y,z,w,v,u,f

Detailed syntax breakdown of Definition df-plq

Step	Hyp	Ref	Expression
1		cplq 4968	. 2 class +Q
2		vx	. . . . . . 7 set x
3	2	cv 954	. . . . . 6 class x
4		cnq 4966	. . . . . 6 class Q.
5	3, 4	wcel 957	. . . . 5 wff x e. Q.
6		vy	. . . . . . 7 set y
7	6	cv 954	. . . . . 6 class y
8	7, 4	wcel 957	. . . . 5 wff y e. Q.
9	5, 8	wa 223	. . . 4 wff (x e. Q. /\ y e. Q.)
10		vw	. . . . . . . . . . . . . 14 set w
11	10	cv 954	. . . . . . . . . . . . 13 class w
12		vv	. . . . . . . . . . . . . 14 set v
13	12	cv 954	. . . . . . . . . . . . 13 class v
14	11, 13	cop 2409	. . . . . . . . . . . 12 class <.w, v>.
15		ceq 4965	. . . . . . . . . . . 12 class ~Q
16	14, 15	cec 4256	. . . . . . . . . . 11 class [<.w, v>.] ~Q
17	3, 16	wceq 955	. . . . . . . . . 10 wff x = [<.w, v>.] ~Q
18		vu	. . . . . . . . . . . . . 14 set u
19	18	cv 954	. . . . . . . . . . . . 13 class u
20		vf	. . . . . . . . . . . . . 14 set f
21	20	cv 954	. . . . . . . . . . . . 13 class f
22	19, 21	cop 2409	. . . . . . . . . . . 12 class <.u, f>.
23	22, 15	cec 4256	. . . . . . . . . . 11 class [<.u, f>.] ~Q
24	7, 23	wceq 955	. . . . . . . . . 10 wff y = [<.u, f>.] ~Q
25	17, 24	wa 223	. . . . . . . . 9 wff (x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q )
26		vz	. . . . . . . . . . 11 set z
27	26	cv 954	. . . . . . . . . 10 class z
28		cplpq 4963	. . . . . . . . . . . 12 class +pQ
29	14, 22, 28	co 3960	. . . . . . . . . . 11 class (<.w, v>. +pQ <.u, f>.)
30	29, 15	cec 4256	. . . . . . . . . 10 class [(<.w, v>. +pQ <.u, f>.)] ~Q
31	27, 30	wceq 955	. . . . . . . . 9 wff z = [(<.w, v>. +pQ <.u, f>.)] ~Q
32	25, 31	wa 223	. . . . . . . 8 wff ((x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q ) /\ z = [(<.w, v>. +pQ <.u, f>.)] ~Q )
33	32, 20	wex 979	. . . . . . 7 wff E.f((x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q ) /\ z = [(<.w, v>. +pQ <.u, f>.)] ~Q )
34	33, 18	wex 979	. . . . . 6 wff E.uE.f((x = [<.w, v>.] ~Q /\ y = [<.u, f>.] ~Q ) /\ z = [(<.w, v>. +pQ <.u, f>.)] ~Q )
35	34, 12	wex 979	. . . . 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 979	. . . 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 223	. . 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 3961	. 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 955	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:  addpipq 5041  dmaddpq 5046

Copyright terms: Public domain