Definition df-imp 7688

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7687 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 7513	. 2 class .P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7510	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1396	. . . . . . . . 9 class r
7	2	cv 1396	. . . . . . . . . 10 class x
8		c1st 6300	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5326	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2202	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1396	. . . . . . . . 9 class s
13	3	cv 1396	. . . . . . . . . 10 class y
14	13, 8	cfv 5326	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2202	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1396	. . . . . . . . 9 class q
18		cmq 7502	. . . . . . . . . 10 class .Q
19	6, 12, 18	co 6017	. . . . . . . . 9 class ( r .Q s )
20	17, 19	wceq 1397	. . . . . . . 8 wff q = ( r .Q s )
21	10, 15, 20	w3a 1004	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
22		cnq 7499	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2511	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
24	23, 5, 22	wrex 2511	. . . . 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 2514	. . . 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 6301	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5326	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2202	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5326	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2202	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 1004	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
32	31, 11, 22	wrex 2511	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
33	32, 5, 22	wrex 2511	. . . . 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 2514	. . . 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 3672	. . 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 6019	. 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 1397	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  7758  dmmp  7760  mulnqprl  7787  mulnqpru  7788  mulclpr  7791  mulnqprlemrl  7792  mulnqprlemru  7793  mulassprg  7800  distrlem1prl  7801  distrlem1pru  7802  distrlem4prl  7803  distrlem4pru  7804  distrlem5prl  7805  distrlem5pru  7806  1idprl  7809  1idpru  7810  recexprlem1ssl  7852  recexprlem1ssu  7853  recexprlemss1l  7854  recexprlemss1u  7855