Definition df-plpq 5035

Description: Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 5240, and is intended to be used only by the construction. This "pre-addition" operation works works directly with ordered pairs of integers. The actual positive fraction addition +Q (df-plq 5039) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 5037). (Analogous remarks apply to the other "pre-" operations in the complex number construction that follows.) From Proposition 9-2.3 of [Gleason] p. 117.

Assertion

Ref	Expression
df-plpq	|- +pQ = {<.<.x, y>., z>. | ((x e. (N. X. N.) /\ y e. (N. X. N.)) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .N f) +N (v .N u)), (v .N f)>.))}

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

Detailed syntax breakdown of Definition df-plpq

Step	Hyp	Ref	Expression
1		cplpq 4976	. 2 class +pQ
2		vx	. . . . . . 7 set x
3	2	cv 955	. . . . . 6 class x
4		cnpi 4972	. . . . . . 7 class N.
5	4, 4	cxp 3168	. . . . . 6 class (N. X. N.)
6	3, 5	wcel 958	. . . . 5 wff x e. (N. X. N.)
7		vy	. . . . . . 7 set y
8	7	cv 955	. . . . . 6 class y
9	8, 5	wcel 958	. . . . 5 wff y e. (N. X. N.)
10	6, 9	wa 223	. . . 4 wff (x e. (N. X. N.) /\ y e. (N. X. N.))
11		vw	. . . . . . . . . . . . 13 set w
12	11	cv 955	. . . . . . . . . . . 12 class w
13		vv	. . . . . . . . . . . . 13 set v
14	13	cv 955	. . . . . . . . . . . 12 class v
15	12, 14	cop 2411	. . . . . . . . . . 11 class <.w, v>.
16	3, 15	wceq 956	. . . . . . . . . 10 wff x = <.w, v>.
17		vu	. . . . . . . . . . . . 13 set u
18	17	cv 955	. . . . . . . . . . . 12 class u
19		vf	. . . . . . . . . . . . 13 set f
20	19	cv 955	. . . . . . . . . . . 12 class f
21	18, 20	cop 2411	. . . . . . . . . . 11 class <.u, f>.
22	8, 21	wceq 956	. . . . . . . . . 10 wff y = <.u, f>.
23	16, 22	wa 223	. . . . . . . . 9 wff (x = <.w, v>. /\ y = <.u, f>.)
24		vz	. . . . . . . . . . 11 set z
25	24	cv 955	. . . . . . . . . 10 class z
26		cmi 4974	. . . . . . . . . . . . 13 class .N
27	12, 20, 26	co 3963	. . . . . . . . . . . 12 class (w .N f)
28	14, 18, 26	co 3963	. . . . . . . . . . . 12 class (v .N u)
29		cpli 4973	. . . . . . . . . . . 12 class +N
30	27, 28, 29	co 3963	. . . . . . . . . . 11 class ((w .N f) +N (v .N u))
31	14, 20, 26	co 3963	. . . . . . . . . . 11 class (v .N f)
32	30, 31	cop 2411	. . . . . . . . . 10 class <.((w .N f) +N (v .N u)), (v .N f)>.
33	25, 32	wceq 956	. . . . . . . . 9 wff z = <.((w .N f) +N (v .N u)), (v .N f)>.
34	23, 33	wa 223	. . . . . . . 8 wff ((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .N f) +N (v .N u)), (v .N f)>.)
35	34, 19	wex 980	. . . . . . 7 wff E.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .N f) +N (v .N u)), (v .N f)>.)
36	35, 17	wex 980	. . . . . 6 wff E.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .N f) +N (v .N u)), (v .N f)>.)
37	36, 13	wex 980	. . . . 5 wff E.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .N f) +N (v .N u)), (v .N f)>.)
38	37, 11	wex 980	. . . 4 wff E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .N f) +N (v .N u)), (v .N f)>.)
39	10, 38	wa 223	. . 3 wff ((x e. (N. X. N.) /\ y e. (N. X. N.)) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .N f) +N (v .N u)), (v .N f)>.))
40	39, 2, 7, 24	copab2 3964	. 2 class {<.<.x, y>., z>. | ((x e. (N. X. N.) /\ y e. (N. X. N.)) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .N f) +N (v .N u)), (v .N f)>.))}
41	1, 40	wceq 956	1 wff +pQ = {<.<.x, y>., z>. | ((x e. (N. X. N.) /\ y e. (N. X. N.)) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .N f) +N (v .N u)), (v .N f)>.))}

This definition is referenced by:  addpipq 5054

Copyright terms: Public domain