Definition df-plq0 7425

Description: Define addition on nonnegative 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 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q0 ∧ 𝑦 ∈ Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0 ))}

Distinct variable group:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑓

Detailed syntax breakdown of Definition df-plq0

Step	Hyp	Ref	Expression
1		cplq0 7287	. 2 class +Q0
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1352	. . . . . 6 class 𝑥
4		cnq0 7285	. . . . . 6 class Q0
5	3, 4	wcel 2148	. . . . 5 wff 𝑥 ∈ Q0
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1352	. . . . . 6 class 𝑦
8	7, 4	wcel 2148	. . . . 5 wff 𝑦 ∈ Q0
9	5, 8	wa 104	. . . 4 wff (𝑥 ∈ Q0 ∧ 𝑦 ∈ Q0)
10		vw	. . . . . . . . . . . . . 14 setvar 𝑤
11	10	cv 1352	. . . . . . . . . . . . 13 class 𝑤
12		vv	. . . . . . . . . . . . . 14 setvar 𝑣
13	12	cv 1352	. . . . . . . . . . . . 13 class 𝑣
14	11, 13	cop 3595	. . . . . . . . . . . 12 class ⟨𝑤, 𝑣⟩
15		ceq0 7284	. . . . . . . . . . . 12 class ~Q0
16	14, 15	cec 6532	. . . . . . . . . . 11 class [⟨𝑤, 𝑣⟩] ~Q0
17	3, 16	wceq 1353	. . . . . . . . . 10 wff 𝑥 = [⟨𝑤, 𝑣⟩] ~Q0
18		vu	. . . . . . . . . . . . . 14 setvar 𝑢
19	18	cv 1352	. . . . . . . . . . . . 13 class 𝑢
20		vf	. . . . . . . . . . . . . 14 setvar 𝑓
21	20	cv 1352	. . . . . . . . . . . . 13 class 𝑓
22	19, 21	cop 3595	. . . . . . . . . . . 12 class ⟨𝑢, 𝑓⟩
23	22, 15	cec 6532	. . . . . . . . . . 11 class [⟨𝑢, 𝑓⟩] ~Q0
24	7, 23	wceq 1353	. . . . . . . . . 10 wff 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0
25	17, 24	wa 104	. . . . . . . . 9 wff (𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 )
26		vz	. . . . . . . . . . 11 setvar 𝑧
27	26	cv 1352	. . . . . . . . . 10 class 𝑧
28		comu 6414	. . . . . . . . . . . . . 14 class ·o
29	11, 21, 28	co 5874	. . . . . . . . . . . . 13 class (𝑤 ·o 𝑓)
30	13, 19, 28	co 5874	. . . . . . . . . . . . 13 class (𝑣 ·o 𝑢)
31		coa 6413	. . . . . . . . . . . . 13 class +o
32	29, 30, 31	co 5874	. . . . . . . . . . . 12 class ((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢))
33	13, 21, 28	co 5874	. . . . . . . . . . . 12 class (𝑣 ·o 𝑓)
34	32, 33	cop 3595	. . . . . . . . . . 11 class ⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩
35	34, 15	cec 6532	. . . . . . . . . 10 class [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0
36	27, 35	wceq 1353	. . . . . . . . 9 wff 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0
37	25, 36	wa 104	. . . . . . . 8 wff ((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0 )
38	37, 20	wex 1492	. . . . . . 7 wff ∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0 )
39	38, 18	wex 1492	. . . . . 6 wff ∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0 )
40	39, 12	wex 1492	. . . . 5 wff ∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0 )
41	40, 10	wex 1492	. . . 4 wff ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0 )
42	9, 41	wa 104	. . 3 wff ((𝑥 ∈ Q0 ∧ 𝑦 ∈ Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0 ))
43	42, 2, 6, 26	coprab 5875	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q0 ∧ 𝑦 ∈ Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0 ))}
44	1, 43	wceq 1353	1 wff +Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q0 ∧ 𝑦 ∈ Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0 ))}

This definition is referenced by:  dfplq0qs  7428