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	$⊢ +_{𝑹} = \{⟨⟨x, y⟩, z⟩ \| ((x \in 𝑹 \land y \in 𝑹) \land \exists w \exists v \exists u \exists f ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, f⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} f⟩] ~_{𝑹}))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplr	$class +_{𝑹}$
1		vx	$setvar x$
2		vy	$setvar y$
3		vz	$setvar z$
4	1	cv	$setvar x$
5		cnr	$class 𝑹$
6	4 5	wcel	$wff x \in 𝑹$
7	2	cv	$setvar y$
8	7 5	wcel	$wff y \in 𝑹$
9	6 8	wa	$wff (x \in 𝑹 \land y \in 𝑹)$
10		vw	$setvar w$
11		vv	$setvar v$
12		vu	$setvar u$
13		vf	$setvar f$
14	10	cv	$setvar w$
15	11	cv	$setvar v$
16	14 15	cop	$class ⟨w, v⟩$
17		cer	$class ~_{𝑹}$
18	16 17	cec	$class [⟨w, v⟩] ~_{𝑹}$
19	4 18	wceq	$wff x = [⟨w, v⟩] ~_{𝑹}$
20	12	cv	$setvar u$
21	13	cv	$setvar f$
22	20 21	cop	$class ⟨u, f⟩$
23	22 17	cec	$class [⟨u, f⟩] ~_{𝑹}$
24	7 23	wceq	$wff y = [⟨u, f⟩] ~_{𝑹}$
25	19 24	wa	$wff (x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, f⟩] ~_{𝑹})$
26	3	cv	$setvar z$
27		cpp	$class +_{𝑷}$
28	14 20 27	co	$class (w +_{𝑷} u)$
29	15 21 27	co	$class (v +_{𝑷} f)$
30	28 29	cop	$class ⟨w +_{𝑷} u, v +_{𝑷} f⟩$
31	30 17	cec	$class [⟨w +_{𝑷} u, v +_{𝑷} f⟩] ~_{𝑹}$
32	26 31	wceq	$wff z = [⟨w +_{𝑷} u, v +_{𝑷} f⟩] ~_{𝑹}$
33	25 32	wa	$wff ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, f⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} f⟩] ~_{𝑹})$
34	33 13	wex	$wff \exists f ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, f⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} f⟩] ~_{𝑹})$
35	34 12	wex	$wff \exists u \exists f ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, f⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} f⟩] ~_{𝑹})$
36	35 11	wex	$wff \exists v \exists u \exists f ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, f⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} f⟩] ~_{𝑹})$
37	36 10	wex	$wff \exists w \exists v \exists u \exists f ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, f⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} f⟩] ~_{𝑹})$
38	9 37	wa	$wff ((x \in 𝑹 \land y \in 𝑹) \land \exists w \exists v \exists u \exists f ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, f⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} f⟩] ~_{𝑹}))$
39	38 1 2 3	coprab	$class \{⟨⟨x, y⟩, z⟩ \| ((x \in 𝑹 \land y \in 𝑹) \land \exists w \exists v \exists u \exists f ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, f⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} f⟩] ~_{𝑹}))\}$
40	0 39	wceq	$wff +_{𝑹} = \{⟨⟨x, y⟩, z⟩ \| ((x \in 𝑹 \land y \in 𝑹) \land \exists w \exists v \exists u \exists f ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, f⟩] ~_{𝑹}) \land z = [⟨w +_{𝑷} u, v +_{𝑷} f⟩] ~_{𝑹}))\}$

Metamath Proof Explorer

Definition df-plr

Detailed syntax breakdown