Definition df-imp 7836

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7835 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 7661	. 2 class .P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7658	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1401	. . . . . . . . 9 class r
7	2	cv 1401	. . . . . . . . . 10 class x
8		c1st 6372	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5377	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2209	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1401	. . . . . . . . 9 class s
13	3	cv 1401	. . . . . . . . . 10 class y
14	13, 8	cfv 5377	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2209	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1401	. . . . . . . . 9 class q
18		cmq 7650	. . . . . . . . . 10 class .Q
19	6, 12, 18	co 6085	. . . . . . . . 9 class ( r .Q s )
20	17, 19	wceq 1402	. . . . . . . 8 wff q = ( r .Q s )
21	10, 15, 20	w3a 1009	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
22		cnq 7647	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2529	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
24	23, 5, 22	wrex 2529	. . . . 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 2532	. . . 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 6373	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5377	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2209	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5377	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2209	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 1009	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
32	31, 11, 22	wrex 2529	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
33	32, 5, 22	wrex 2529	. . . . 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 2532	. . . 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 3712	. . 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 6087	. 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 1402	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 used by:  mpvlu  7906  dmmp  7908  mulnqprl  7935  mulnqpru  7936  mulclpr  7939  mulnqprlemrl  7940  mulnqprlemru  7941  mulassprg  7948  distrlem1prl  7949  distrlem1pru  7950  distrlem4prl  7951  distrlem4pru  7952  distrlem5prl  7953  distrlem5pru  7954  1idprl  7957  1idpru  7958  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  recexprlemss1u  8003