Definition df-imp 7270

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7269 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 7095	. 2 class .P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7092	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1330	. . . . . . . . 9 class r
7	2	cv 1330	. . . . . . . . . 10 class x
8		c1st 6029	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5118	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 1480	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1330	. . . . . . . . 9 class s
13	3	cv 1330	. . . . . . . . . 10 class y
14	13, 8	cfv 5118	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 1480	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1330	. . . . . . . . 9 class q
18		cmq 7084	. . . . . . . . . 10 class .Q
19	6, 12, 18	co 5767	. . . . . . . . 9 class ( r .Q s )
20	17, 19	wceq 1331	. . . . . . . 8 wff q = ( r .Q s )
21	10, 15, 20	w3a 962	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
22		cnq 7081	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2415	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
24	23, 5, 22	wrex 2415	. . . . 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 2418	. . . 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 6030	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5118	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 1480	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5118	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 1480	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 962	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
32	31, 11, 22	wrex 2415	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
33	32, 5, 22	wrex 2415	. . . . 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 2418	. . . 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 3525	. . 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 5769	. 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 1331	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  7340  dmmp  7342  mulnqprl  7369  mulnqpru  7370  mulclpr  7373  mulnqprlemrl  7374  mulnqprlemru  7375  mulassprg  7382  distrlem1prl  7383  distrlem1pru  7384  distrlem4prl  7385  distrlem4pru  7386  distrlem5prl  7387  distrlem5pru  7388  1idprl  7391  1idpru  7392  recexprlem1ssl  7434  recexprlem1ssu  7435  recexprlemss1l  7436  recexprlemss1u  7437