Definition df-imp 7732

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7731 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 7557	. 2 class .P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7554	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1397	. . . . . . . . 9 class r
7	2	cv 1397	. . . . . . . . . 10 class x
8		c1st 6310	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5333	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2202	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1397	. . . . . . . . 9 class s
13	3	cv 1397	. . . . . . . . . 10 class y
14	13, 8	cfv 5333	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2202	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1397	. . . . . . . . 9 class q
18		cmq 7546	. . . . . . . . . 10 class .Q
19	6, 12, 18	co 6028	. . . . . . . . 9 class ( r .Q s )
20	17, 19	wceq 1398	. . . . . . . 8 wff q = ( r .Q s )
21	10, 15, 20	w3a 1005	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
22		cnq 7543	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2512	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
24	23, 5, 22	wrex 2512	. . . . 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 2515	. . . 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 6311	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5333	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2202	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5333	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2202	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 1005	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
32	31, 11, 22	wrex 2512	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
33	32, 5, 22	wrex 2512	. . . . 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 2515	. . . 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 3676	. . 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 6030	. 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 1398	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  7802  dmmp  7804  mulnqprl  7831  mulnqpru  7832  mulclpr  7835  mulnqprlemrl  7836  mulnqprlemru  7837  mulassprg  7844  distrlem1prl  7845  distrlem1pru  7846  distrlem4prl  7847  distrlem4pru  7848  distrlem5prl  7849  distrlem5pru  7850  1idprl  7853  1idpru  7854  recexprlem1ssl  7896  recexprlem1ssu  7897  recexprlemss1l  7898  recexprlemss1u  7899