Definition df-imp 7612

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7611 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 7437	. 2 class .P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7434	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1372	. . . . . . . . 9 class r
7	2	cv 1372	. . . . . . . . . 10 class x
8		c1st 6242	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5285	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2177	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1372	. . . . . . . . 9 class s
13	3	cv 1372	. . . . . . . . . 10 class y
14	13, 8	cfv 5285	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2177	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1372	. . . . . . . . 9 class q
18		cmq 7426	. . . . . . . . . 10 class .Q
19	6, 12, 18	co 5962	. . . . . . . . 9 class ( r .Q s )
20	17, 19	wceq 1373	. . . . . . . 8 wff q = ( r .Q s )
21	10, 15, 20	w3a 981	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
22		cnq 7423	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2486	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
24	23, 5, 22	wrex 2486	. . . . 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 2489	. . . 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 6243	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5285	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2177	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5285	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2177	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 981	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
32	31, 11, 22	wrex 2486	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
33	32, 5, 22	wrex 2486	. . . . 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 2489	. . . 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 3641	. . 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 5964	. 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 1373	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  7682  dmmp  7684  mulnqprl  7711  mulnqpru  7712  mulclpr  7715  mulnqprlemrl  7716  mulnqprlemru  7717  mulassprg  7724  distrlem1prl  7725  distrlem1pru  7726  distrlem4prl  7727  distrlem4pru  7728  distrlem5prl  7729  distrlem5pru  7730  1idprl  7733  1idpru  7734  recexprlem1ssl  7776  recexprlem1ssu  7777  recexprlemss1l  7778  recexprlemss1u  7779