Definition df-mr 7796

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

Assertion

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

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

Detailed syntax breakdown of Definition df-mr

Step	Hyp	Ref	Expression
1		cmr 7369	. 2 class .R
2		vx	. . . . . . 7 setvar x
3	2	cv 1363	. . . . . 6 class x
4		cnr 7364	. . . . . 6 class R.
5	3, 4	wcel 2167	. . . . 5 wff x e. R.
6		vy	. . . . . . 7 setvar y
7	6	cv 1363	. . . . . 6 class y
8	7, 4	wcel 2167	. . . . 5 wff y e. R.
9	5, 8	wa 104	. . . 4 wff ( x e. R. /\ y e. R. )
10		vw	. . . . . . . . . . . . . 14 setvar w
11	10	cv 1363	. . . . . . . . . . . . 13 class w
12		vv	. . . . . . . . . . . . . 14 setvar v
13	12	cv 1363	. . . . . . . . . . . . 13 class v
14	11, 13	cop 3625	. . . . . . . . . . . 12 class <. w , v >.
15		cer 7363	. . . . . . . . . . . 12 class ~R
16	14, 15	cec 6590	. . . . . . . . . . 11 class [ <. w , v >. ] ~R
17	3, 16	wceq 1364	. . . . . . . . . 10 wff x = [ <. w , v >. ] ~R
18		vu	. . . . . . . . . . . . . 14 setvar u
19	18	cv 1363	. . . . . . . . . . . . 13 class u
20		vf	. . . . . . . . . . . . . 14 setvar f
21	20	cv 1363	. . . . . . . . . . . . 13 class f
22	19, 21	cop 3625	. . . . . . . . . . . 12 class <. u , f >.
23	22, 15	cec 6590	. . . . . . . . . . 11 class [ <. u , f >. ] ~R
24	7, 23	wceq 1364	. . . . . . . . . 10 wff y = [ <. u , f >. ] ~R
25	17, 24	wa 104	. . . . . . . . 9 wff ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R )
26		vz	. . . . . . . . . . 11 setvar z
27	26	cv 1363	. . . . . . . . . 10 class z
28		cmp 7361	. . . . . . . . . . . . . 14 class .P.
29	11, 19, 28	co 5922	. . . . . . . . . . . . 13 class ( w .P. u )
30	13, 21, 28	co 5922	. . . . . . . . . . . . 13 class ( v .P. f )
31		cpp 7360	. . . . . . . . . . . . 13 class +P.
32	29, 30, 31	co 5922	. . . . . . . . . . . 12 class ( ( w .P. u ) +P. ( v .P. f ) )
33	11, 21, 28	co 5922	. . . . . . . . . . . . 13 class ( w .P. f )
34	13, 19, 28	co 5922	. . . . . . . . . . . . 13 class ( v .P. u )
35	33, 34, 31	co 5922	. . . . . . . . . . . 12 class ( ( w .P. f ) +P. ( v .P. u ) )
36	32, 35	cop 3625	. . . . . . . . . . 11 class <. ( ( w .P. u ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >.
37	36, 15	cec 6590	. . . . . . . . . 10 class [ <. ( ( w .P. u ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~R
38	27, 37	wceq 1364	. . . . . . . . 9 wff z = [ <. ( ( w .P. u ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~R
39	25, 38	wa 104	. . . . . . . 8 wff ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( ( w .P. u ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~R )
40	39, 20	wex 1506	. . . . . . 7 wff E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( ( w .P. u ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~R )
41	40, 18	wex 1506	. . . . . 6 wff E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( ( w .P. u ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~R )
42	41, 12	wex 1506	. . . . 5 wff E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( ( w .P. u ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~R )
43	42, 10	wex 1506	. . . 4 wff E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( ( w .P. u ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~R )
44	9, 43	wa 104	. . 3 wff ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( ( w .P. u ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~R ) )
45	44, 2, 6, 26	coprab 5923	. 2 class { <. <. x , y >. , z >. | ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( ( w .P. u ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~R ) ) }
46	1, 45	wceq 1364	1 wff .R = { <. <. x , y >. , z >. | ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( ( w .P. u ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~R ) ) }

This definition is referenced by:  mulsrpr  7813