Definition df-imp 7582

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7581 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 7407	. 2 class .P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7404	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1372	. . . . . . . . 9 class r
7	2	cv 1372	. . . . . . . . . 10 class x
8		c1st 6224	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5271	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2176	. . . . . . . 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 5271	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2176	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1372	. . . . . . . . 9 class q
18		cmq 7396	. . . . . . . . . 10 class .Q
19	6, 12, 18	co 5944	. . . . . . . . 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 7393	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2485	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
24	23, 5, 22	wrex 2485	. . . . 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 2488	. . . 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 6225	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5271	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2176	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5271	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2176	. . . . . . . 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 2485	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
33	32, 5, 22	wrex 2485	. . . . 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 2488	. . . 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 3636	. . 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 5946	. 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  7652  dmmp  7654  mulnqprl  7681  mulnqpru  7682  mulclpr  7685  mulnqprlemrl  7686  mulnqprlemru  7687  mulassprg  7694  distrlem1prl  7695  distrlem1pru  7696  distrlem4prl  7697  distrlem4pru  7698  distrlem5prl  7699  distrlem5pru  7700  1idprl  7703  1idpru  7704  recexprlem1ssl  7746  recexprlem1ssu  7747  recexprlemss1l  7748  recexprlemss1u  7749