Definition df-plq0 6409

Description: Define addition on non-negative fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 2-Nov-2019.)

Assertion

Ref	Expression
df-plq0	⊢ +Q0 = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ Q0 ∧ y ∈ Q0) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~Q0 ∧ y = [⟨u, f⟩] ~Q0 ) ∧ z = [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0 ))}

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

Detailed syntax breakdown of Definition df-plq0

Step	Hyp	Ref	Expression
1		cplq0 6273	. 2 class +Q0
2		vx	. . . . . . 7 setvar x
3	2	cv 1241	. . . . . 6 class x
4		cnq0 6271	. . . . . 6 class Q0
5	3, 4	wcel 1390	. . . . 5 wff x ∈ Q0
6		vy	. . . . . . 7 setvar y
7	6	cv 1241	. . . . . 6 class y
8	7, 4	wcel 1390	. . . . 5 wff y ∈ Q0
9	5, 8	wa 97	. . . 4 wff (x ∈ Q0 ∧ y ∈ Q0)
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 3370	. . . . . . . . . . . 12 class ⟨w, v⟩
15		ceq0 6270	. . . . . . . . . . . 12 class ~Q0
16	14, 15	cec 6040	. . . . . . . . . . 11 class [⟨w, v⟩] ~Q0
17	3, 16	wceq 1242	. . . . . . . . . 10 wff x = [⟨w, v⟩] ~Q0
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 3370	. . . . . . . . . . . 12 class ⟨u, f⟩
23	22, 15	cec 6040	. . . . . . . . . . 11 class [⟨u, f⟩] ~Q0
24	7, 23	wceq 1242	. . . . . . . . . 10 wff y = [⟨u, f⟩] ~Q0
25	17, 24	wa 97	. . . . . . . . 9 wff (x = [⟨w, v⟩] ~Q0 ∧ y = [⟨u, f⟩] ~Q0 )
26		vz	. . . . . . . . . . 11 setvar z
27	26	cv 1241	. . . . . . . . . 10 class z
28		comu 5938	. . . . . . . . . . . . . 14 class ·𝑜
29	11, 21, 28	co 5455	. . . . . . . . . . . . 13 class (w ·𝑜 f)
30	13, 19, 28	co 5455	. . . . . . . . . . . . 13 class (v ·𝑜 u)
31		coa 5937	. . . . . . . . . . . . 13 class +𝑜
32	29, 30, 31	co 5455	. . . . . . . . . . . 12 class ((w ·𝑜 f) +𝑜 (v ·𝑜 u))
33	13, 21, 28	co 5455	. . . . . . . . . . . 12 class (v ·𝑜 f)
34	32, 33	cop 3370	. . . . . . . . . . 11 class ⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩
35	34, 15	cec 6040	. . . . . . . . . 10 class [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0
36	27, 35	wceq 1242	. . . . . . . . 9 wff z = [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0
37	25, 36	wa 97	. . . . . . . 8 wff ((x = [⟨w, v⟩] ~Q0 ∧ y = [⟨u, f⟩] ~Q0 ) ∧ z = [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0 )
38	37, 20	wex 1378	. . . . . . 7 wff ∃f((x = [⟨w, v⟩] ~Q0 ∧ y = [⟨u, f⟩] ~Q0 ) ∧ z = [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0 )
39	38, 18	wex 1378	. . . . . 6 wff ∃u∃f((x = [⟨w, v⟩] ~Q0 ∧ y = [⟨u, f⟩] ~Q0 ) ∧ z = [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0 )
40	39, 12	wex 1378	. . . . 5 wff ∃v∃u∃f((x = [⟨w, v⟩] ~Q0 ∧ y = [⟨u, f⟩] ~Q0 ) ∧ z = [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0 )
41	40, 10	wex 1378	. . . 4 wff ∃w∃v∃u∃f((x = [⟨w, v⟩] ~Q0 ∧ y = [⟨u, f⟩] ~Q0 ) ∧ z = [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0 )
42	9, 41	wa 97	. . 3 wff ((x ∈ Q0 ∧ y ∈ Q0) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~Q0 ∧ y = [⟨u, f⟩] ~Q0 ) ∧ z = [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0 ))
43	42, 2, 6, 26	coprab 5456	. 2 class {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ Q0 ∧ y ∈ Q0) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~Q0 ∧ y = [⟨u, f⟩] ~Q0 ) ∧ z = [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0 ))}
44	1, 43	wceq 1242	1 wff +Q0 = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ Q0 ∧ y ∈ Q0) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~Q0 ∧ y = [⟨u, f⟩] ~Q0 ) ∧ z = [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0 ))}

This definition is referenced by:  dfplq0qs  6412