Definition df-imp 7581

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7580 or the definition of multiplication on positive reals in Metamath Proof Explorer. This is as opposed to the more complicated definition of multiplication given in Section 11.2.1 of [HoTT], p. (varies), which appears to be motivated by handling negative numbers or handling modified Dedekind cuts in which locatedness is omitted.

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, 29-Sep-2019.)

Assertion

Ref	Expression
df-imp	|- .P. = ( x e. P. , y e. P. |-> <. { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) ) } , { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) ) } >. )

Distinct variable group:   x, y, q, r, s

Detailed syntax breakdown of Definition df-imp

Step	Hyp	Ref	Expression
1		cmp 7406	. 2 class .P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7403	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1371	. . . . . . . . 9 class r
7	2	cv 1371	. . . . . . . . . 10 class x
8		c1st 6223	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5270	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2175	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1371	. . . . . . . . 9 class s
13	3	cv 1371	. . . . . . . . . 10 class y
14	13, 8	cfv 5270	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2175	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1371	. . . . . . . . 9 class q
18		cmq 7395	. . . . . . . . . 10 class .Q
19	6, 12, 18	co 5943	. . . . . . . . 9 class ( r .Q s )
20	17, 19	wceq 1372	. . . . . . . 8 wff q = ( r .Q s )
21	10, 15, 20	w3a 980	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
22		cnq 7392	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2484	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
24	23, 5, 22	wrex 2484	. . . . 5 wff E. r e. Q. E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
25	24, 16, 22	crab 2487	. . . 4 class { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) ) }
26		c2nd 6224	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5270	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2175	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5270	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2175	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 980	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
32	31, 11, 22	wrex 2484	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
33	32, 5, 22	wrex 2484	. . . . 5 wff E. r e. Q. E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
34	33, 16, 22	crab 2487	. . . 4 class { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) ) }
35	25, 34	cop 3635	. . 3 class <. { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) ) } , { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) ) } >.
36	2, 3, 4, 4, 35	cmpo 5945	. 2 class ( x e. P. , y e. P. |-> <. { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) ) } , { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) ) } >. )
37	1, 36	wceq 1372	1 wff .P. = ( x e. P. , y e. P. |-> <. { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) ) } , { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) ) } >. )

This definition is referenced by:  mpvlu  7651  dmmp  7653  mulnqprl  7680  mulnqpru  7681  mulclpr  7684  mulnqprlemrl  7685  mulnqprlemru  7686  mulassprg  7693  distrlem1prl  7694  distrlem1pru  7695  distrlem4prl  7696  distrlem4pru  7697  distrlem5prl  7698  distrlem5pru  7699  1idprl  7702  1idpru  7703  recexprlem1ssl  7745  recexprlem1ssu  7746  recexprlemss1l  7747  recexprlemss1u  7748