Definition df-imp 7089

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7088 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 6914	. 2 class .P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 6911	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1289	. . . . . . . . 9 class r
7	2	cv 1289	. . . . . . . . . 10 class x
8		c1st 5923	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5028	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 1439	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1289	. . . . . . . . 9 class s
13	3	cv 1289	. . . . . . . . . 10 class y
14	13, 8	cfv 5028	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 1439	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1289	. . . . . . . . 9 class q
18		cmq 6903	. . . . . . . . . 10 class .Q
19	6, 12, 18	co 5666	. . . . . . . . 9 class ( r .Q s )
20	17, 19	wceq 1290	. . . . . . . 8 wff q = ( r .Q s )
21	10, 15, 20	w3a 925	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
22		cnq 6900	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2361	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
24	23, 5, 22	wrex 2361	. . . . 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 2364	. . . 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 5924	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5028	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 1439	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5028	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 1439	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 925	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
32	31, 11, 22	wrex 2361	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
33	32, 5, 22	wrex 2361	. . . . 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 2364	. . . 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 3453	. . 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	cmpt2 5668	. 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 1290	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  7159  dmmp  7161  mulnqprl  7188  mulnqpru  7189  mulclpr  7192  mulnqprlemrl  7193  mulnqprlemru  7194  mulassprg  7201  distrlem1prl  7202  distrlem1pru  7203  distrlem4prl  7204  distrlem4pru  7205  distrlem5prl  7206  distrlem5pru  7207  1idprl  7210  1idpru  7211  recexprlem1ssl  7253  recexprlem1ssu  7254  recexprlemss1l  7255  recexprlemss1u  7256