Definition df-plr

Description: Define addition on signed reals. This is a "temporary" set used in the construction of complex numbers df-c , 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.)

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

Detailed syntax breakdown

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