Definition df-mq0 7390

Description: Define multiplication on nonnegative fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 2-Nov-2019.)

Assertion

Ref	Expression
df-mq0	|- ·Q0 = { <. <. x , y >. , z >. | ( ( x e. Q0 /\ y e. Q0 ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~Q0 /\ y = [ <. u , f >. ] ~Q0 ) /\ z = [ <. ( w .o u ) , ( v .o f ) >. ] ~Q0 ) ) }

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

Detailed syntax breakdown of Definition df-mq0

Step	Hyp	Ref	Expression
1		cmq0 7252	. 2 class ·Q0
2		vx	. . . . . . 7 setvar x
3	2	cv 1347	. . . . . 6 class x
4		cnq0 7249	. . . . . 6 class Q0
5	3, 4	wcel 2141	. . . . 5 wff x e. Q0
6		vy	. . . . . . 7 setvar y
7	6	cv 1347	. . . . . 6 class y
8	7, 4	wcel 2141	. . . . 5 wff y e. Q0
9	5, 8	wa 103	. . . 4 wff ( x e. Q0 /\ y e. Q0 )
10		vw	. . . . . . . . . . . . . 14 setvar w
11	10	cv 1347	. . . . . . . . . . . . 13 class w
12		vv	. . . . . . . . . . . . . 14 setvar v
13	12	cv 1347	. . . . . . . . . . . . 13 class v
14	11, 13	cop 3586	. . . . . . . . . . . 12 class <. w , v >.
15		ceq0 7248	. . . . . . . . . . . 12 class ~Q0
16	14, 15	cec 6511	. . . . . . . . . . 11 class [ <. w , v >. ] ~Q0
17	3, 16	wceq 1348	. . . . . . . . . 10 wff x = [ <. w , v >. ] ~Q0
18		vu	. . . . . . . . . . . . . 14 setvar u
19	18	cv 1347	. . . . . . . . . . . . 13 class u
20		vf	. . . . . . . . . . . . . 14 setvar f
21	20	cv 1347	. . . . . . . . . . . . 13 class f
22	19, 21	cop 3586	. . . . . . . . . . . 12 class <. u , f >.
23	22, 15	cec 6511	. . . . . . . . . . 11 class [ <. u , f >. ] ~Q0
24	7, 23	wceq 1348	. . . . . . . . . 10 wff y = [ <. u , f >. ] ~Q0
25	17, 24	wa 103	. . . . . . . . 9 wff ( x = [ <. w , v >. ] ~Q0 /\ y = [ <. u , f >. ] ~Q0 )
26		vz	. . . . . . . . . . 11 setvar z
27	26	cv 1347	. . . . . . . . . 10 class z
28		comu 6393	. . . . . . . . . . . . 13 class .o
29	11, 19, 28	co 5853	. . . . . . . . . . . 12 class ( w .o u )
30	13, 21, 28	co 5853	. . . . . . . . . . . 12 class ( v .o f )
31	29, 30	cop 3586	. . . . . . . . . . 11 class <. ( w .o u ) , ( v .o f ) >.
32	31, 15	cec 6511	. . . . . . . . . 10 class [ <. ( w .o u ) , ( v .o f ) >. ] ~Q0
33	27, 32	wceq 1348	. . . . . . . . 9 wff z = [ <. ( w .o u ) , ( v .o f ) >. ] ~Q0
34	25, 33	wa 103	. . . . . . . 8 wff ( ( x = [ <. w , v >. ] ~Q0 /\ y = [ <. u , f >. ] ~Q0 ) /\ z = [ <. ( w .o u ) , ( v .o f ) >. ] ~Q0 )
35	34, 20	wex 1485	. . . . . . 7 wff E. f ( ( x = [ <. w , v >. ] ~Q0 /\ y = [ <. u , f >. ] ~Q0 ) /\ z = [ <. ( w .o u ) , ( v .o f ) >. ] ~Q0 )
36	35, 18	wex 1485	. . . . . 6 wff E. u E. f ( ( x = [ <. w , v >. ] ~Q0 /\ y = [ <. u , f >. ] ~Q0 ) /\ z = [ <. ( w .o u ) , ( v .o f ) >. ] ~Q0 )
37	36, 12	wex 1485	. . . . 5 wff E. v E. u E. f ( ( x = [ <. w , v >. ] ~Q0 /\ y = [ <. u , f >. ] ~Q0 ) /\ z = [ <. ( w .o u ) , ( v .o f ) >. ] ~Q0 )
38	37, 10	wex 1485	. . . 4 wff E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~Q0 /\ y = [ <. u , f >. ] ~Q0 ) /\ z = [ <. ( w .o u ) , ( v .o f ) >. ] ~Q0 )
39	9, 38	wa 103	. . 3 wff ( ( x e. Q0 /\ y e. Q0 ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~Q0 /\ y = [ <. u , f >. ] ~Q0 ) /\ z = [ <. ( w .o u ) , ( v .o f ) >. ] ~Q0 ) )
40	39, 2, 6, 26	coprab 5854	. 2 class { <. <. x , y >. , z >. | ( ( x e. Q0 /\ y e. Q0 ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~Q0 /\ y = [ <. u , f >. ] ~Q0 ) /\ z = [ <. ( w .o u ) , ( v .o f ) >. ] ~Q0 ) ) }
41	1, 40	wceq 1348	1 wff ·Q0 = { <. <. x , y >. , z >. | ( ( x e. Q0 /\ y e. Q0 ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~Q0 /\ y = [ <. u , f >. ] ~Q0 ) /\ z = [ <. ( w .o u ) , ( v .o f ) >. ] ~Q0 ) ) }

This definition is referenced by:  dfmq0qs  7391