Definition df-imp 7826

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7825 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 7651	. 2 class .P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7648	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1401	. . . . . . . . 9 class r
7	2	cv 1401	. . . . . . . . . 10 class x
8		c1st 6362	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5372	. . . . . . . . 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 5372	. . . . . . . . 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 7640	. . . . . . . . . 10 class .Q
19	6, 12, 18	co 6075	. . . . . . . . 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 7637	. . . . . . 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 6363	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5372	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2209	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5372	. . . . . . . . 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 3708	. . 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 6077	. 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 referenced by:  mpvlu  7896  dmmp  7898  mulnqprl  7925  mulnqpru  7926  mulclpr  7929  mulnqprlemrl  7930  mulnqprlemru  7931  mulassprg  7938  distrlem1prl  7939  distrlem1pru  7940  distrlem4prl  7941  distrlem4pru  7942  distrlem5prl  7943  distrlem5pru  7944  1idprl  7947  1idpru  7948  recexprlem1ssl  7990  recexprlem1ssu  7991  recexprlemss1l  7992  recexprlemss1u  7993