Definition df-plr 10671

Description: Define addition on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10735, and is intended to be used only by the construction. From Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.)

Assertion

Ref	Expression
df-plr	⊢ +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R ))}

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

Detailed syntax breakdown of Definition df-plr

Step	Hyp	Ref	Expression
1		cplr 10483	. 2 class +R
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1542	. . . . . 6 class 𝑥
4		cnr 10479	. . . . . 6 class R
5	3, 4	wcel 2110	. . . . 5 wff 𝑥 ∈ R
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1542	. . . . . 6 class 𝑦
8	7, 4	wcel 2110	. . . . 5 wff 𝑦 ∈ R
9	5, 8	wa 399	. . . 4 wff (𝑥 ∈ R ∧ 𝑦 ∈ R)
10		vw	. . . . . . . . . . . . . 14 setvar 𝑤
11	10	cv 1542	. . . . . . . . . . . . 13 class 𝑤
12		vv	. . . . . . . . . . . . . 14 setvar 𝑣
13	12	cv 1542	. . . . . . . . . . . . 13 class 𝑣
14	11, 13	cop 4547	. . . . . . . . . . . 12 class ⟨𝑤, 𝑣⟩
15		cer 10478	. . . . . . . . . . . 12 class ~R
16	14, 15	cec 8389	. . . . . . . . . . 11 class [⟨𝑤, 𝑣⟩] ~R
17	3, 16	wceq 1543	. . . . . . . . . 10 wff 𝑥 = [⟨𝑤, 𝑣⟩] ~R
18		vu	. . . . . . . . . . . . . 14 setvar 𝑢
19	18	cv 1542	. . . . . . . . . . . . 13 class 𝑢
20		vf	. . . . . . . . . . . . . 14 setvar 𝑓
21	20	cv 1542	. . . . . . . . . . . . 13 class 𝑓
22	19, 21	cop 4547	. . . . . . . . . . . 12 class ⟨𝑢, 𝑓⟩
23	22, 15	cec 8389	. . . . . . . . . . 11 class [⟨𝑢, 𝑓⟩] ~R
24	7, 23	wceq 1543	. . . . . . . . . 10 wff 𝑦 = [⟨𝑢, 𝑓⟩] ~R
25	17, 24	wa 399	. . . . . . . . 9 wff (𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R )
26		vz	. . . . . . . . . . 11 setvar 𝑧
27	26	cv 1542	. . . . . . . . . 10 class 𝑧
28		cpp 10475	. . . . . . . . . . . . 13 class +P
29	11, 19, 28	co 7213	. . . . . . . . . . . 12 class (𝑤 +P 𝑢)
30	13, 21, 28	co 7213	. . . . . . . . . . . 12 class (𝑣 +P 𝑓)
31	29, 30	cop 4547	. . . . . . . . . . 11 class ⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩
32	31, 15	cec 8389	. . . . . . . . . 10 class [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R
33	27, 32	wceq 1543	. . . . . . . . 9 wff 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R
34	25, 33	wa 399	. . . . . . . 8 wff ((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R )
35	34, 20	wex 1787	. . . . . . 7 wff ∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R )
36	35, 18	wex 1787	. . . . . 6 wff ∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R )
37	36, 12	wex 1787	. . . . 5 wff ∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R )
38	37, 10	wex 1787	. . . 4 wff ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R )
39	9, 38	wa 399	. . 3 wff ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R ))
40	39, 2, 6, 26	coprab 7214	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R ))}
41	1, 40	wceq 1543	1 wff +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R ))}

This definition is referenced by:  addsrpr  10689  dmaddsr  10699