df-mr

Description: Define multiplication 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-mr	$⊢ \cdot_{𝑹} = \{⟨⟨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 \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} f), (w \cdot_{𝑷} f) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmr	$class \cdot_{𝑹}$
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		cmp	$class \cdot_{𝑷}$
28	14 20 27	co	$class (w \cdot_{𝑷} u)$
29		cpp	$class +_{𝑷}$
30	15 21 27	co	$class (v \cdot_{𝑷} f)$
31	28 30 29	co	$class ((w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} f))$
32	14 21 27	co	$class (w \cdot_{𝑷} f)$
33	15 20 27	co	$class (v \cdot_{𝑷} u)$
34	32 33 29	co	$class ((w \cdot_{𝑷} f) +_{𝑷} (v \cdot_{𝑷} u))$
35	31 34	cop	$class ⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} f), (w \cdot_{𝑷} f) +_{𝑷} (v \cdot_{𝑷} u)⟩$
36	35 17	cec	$class [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} f), (w \cdot_{𝑷} f) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}$
37	26 36	wceq	$wff z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} f), (w \cdot_{𝑷} f) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}$
38	25 37	wa	$wff ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, f⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} f), (w \cdot_{𝑷} f) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})$
39	38 13	wex	$wff \exists f ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, f⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} f), (w \cdot_{𝑷} f) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})$
40	39 12	wex	$wff \exists u \exists f ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, f⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} f), (w \cdot_{𝑷} f) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})$
41	40 11	wex	$wff \exists v \exists u \exists f ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, f⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} f), (w \cdot_{𝑷} f) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})$
42	41 10	wex	$wff \exists w \exists v \exists u \exists f ((x = [⟨w, v⟩] ~_{𝑹} \land y = [⟨u, f⟩] ~_{𝑹}) \land z = [⟨(w \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} f), (w \cdot_{𝑷} f) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹})$
43	9 42	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 \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} f), (w \cdot_{𝑷} f) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}))$
44	43 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 \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} f), (w \cdot_{𝑷} f) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}))\}$
45	0 44	wceq	$wff \cdot_{𝑹} = \{⟨⟨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 \cdot_{𝑷} u) +_{𝑷} (v \cdot_{𝑷} f), (w \cdot_{𝑷} f) +_{𝑷} (v \cdot_{𝑷} u)⟩] ~_{𝑹}))\}$

Metamath Proof Explorer

Definition df-mr

Detailed syntax breakdown