Definition df-mr 3963

Description: Define multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 4034, and is intended to be used only by the construction. From Proposition 9-4.3 of [Gleason] p. 126.

Assertion

Ref	Expression
df-mr	|- .R = {<.<.x, y>., z>. | ((x e. R. /\ y e. R.) /\ E.wE.vE.uE.f((x = [<.w, v>.] ~R /\ y = [<.u, f>.] ~R ) /\ z = [(<.w, v>. .pR <.u, f>.)] ~R ))}

Distinct variable group(s):   x,y,z,w,v,u,f

Detailed syntax breakdown of Definition df-mr

Step	Hyp	Ref	Expression
1		cmr 3792	. 2 class .R
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cnr 3787	. . . . . 6 class R.
5	3, 4	wcel 1092	. . . . 5 wff x e. R.
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wcel 1092	. . . . 5 wff y e. R.
9	5, 8	wa 196	. . . 4 wff (x e. R. /\ y e. R.)
10		vw	. . . . . . . . . . . . . 14 set w
11	10	cv 1089	. . . . . . . . . . . . 13 class w
12		vv	. . . . . . . . . . . . . 14 set v
13	12	cv 1089	. . . . . . . . . . . . 13 class v
14	11, 13	cop 1810	. . . . . . . . . . . 12 class <.w, v>.
15		cer 3786	. . . . . . . . . . . 12 class ~R
16	14, 15	cec 3198	. . . . . . . . . . 11 class [<.w, v>.] ~R
17	3, 16	wceq 1091	. . . . . . . . . 10 wff x = [<.w, v>.] ~R
18		vu	. . . . . . . . . . . . . 14 set u
19	18	cv 1089	. . . . . . . . . . . . 13 class u
20		vf	. . . . . . . . . . . . . 14 set f
21	20	cv 1089	. . . . . . . . . . . . 13 class f
22	19, 21	cop 1810	. . . . . . . . . . . 12 class <.u, f>.
23	22, 15	cec 3198	. . . . . . . . . . 11 class [<.u, f>.] ~R
24	7, 23	wceq 1091	. . . . . . . . . 10 wff y = [<.u, f>.] ~R
25	17, 24	wa 196	. . . . . . . . 9 wff (x = [<.w, v>.] ~R /\ y = [<.u, f>.] ~R )
26		vz	. . . . . . . . . . 11 set z
27	26	cv 1089	. . . . . . . . . 10 class z
28		cmpr 3785	. . . . . . . . . . . 12 class .pR
29	14, 22, 28	co 3001	. . . . . . . . . . 11 class (<.w, v>. .pR <.u, f>.)
30	29, 15	cec 3198	. . . . . . . . . 10 class [(<.w, v>. .pR <.u, f>.)] ~R
31	27, 30	wceq 1091	. . . . . . . . 9 wff z = [(<.w, v>. .pR <.u, f>.)] ~R
32	25, 31	wa 196	. . . . . . . 8 wff ((x = [<.w, v>.] ~R /\ y = [<.u, f>.] ~R ) /\ z = [(<.w, v>. .pR <.u, f>.)] ~R )
33	32, 20	wex 678	. . . . . . 7 wff E.f((x = [<.w, v>.] ~R /\ y = [<.u, f>.] ~R ) /\ z = [(<.w, v>. .pR <.u, f>.)] ~R )
34	33, 18	wex 678	. . . . . 6 wff E.uE.f((x = [<.w, v>.] ~R /\ y = [<.u, f>.] ~R ) /\ z = [(<.w, v>. .pR <.u, f>.)] ~R )
35	34, 12	wex 678	. . . . 5 wff E.vE.uE.f((x = [<.w, v>.] ~R /\ y = [<.u, f>.] ~R ) /\ z = [(<.w, v>. .pR <.u, f>.)] ~R )
36	35, 10	wex 678	. . . 4 wff E.wE.vE.uE.f((x = [<.w, v>.] ~R /\ y = [<.u, f>.] ~R ) /\ z = [(<.w, v>. .pR <.u, f>.)] ~R )
37	9, 36	wa 196	. . 3 wff ((x e. R. /\ y e. R.) /\ E.wE.vE.uE.f((x = [<.w, v>.] ~R /\ y = [<.u, f>.] ~R ) /\ z = [(<.w, v>. .pR <.u, f>.)] ~R ))
38	37, 2, 6, 26	copab2 3002	. 2 class {<.<.x, y>., z>. | ((x e. R. /\ y e. R.) /\ E.wE.vE.uE.f((x = [<.w, v>.] ~R /\ y = [<.u, f>.] ~R ) /\ z = [(<.w, v>. .pR <.u, f>.)] ~R ))}
39	1, 38	wceq 1091	1 wff .R = {<.<.x, y>., z>. | ((x e. R. /\ y e. R.) /\ E.wE.vE.uE.f((x = [<.w, v>.] ~R /\ y = [<.u, f>.] ~R ) /\ z = [(<.w, v>. .pR <.u, f>.)] ~R ))}

This definition is referenced by:  mulsrpr 3979  dmmulsr 3989

metamath.org