Definition df-imp 7459

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7458 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 7284	. 2 class .P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7281	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1352	. . . . . . . . 9 class r
7	2	cv 1352	. . . . . . . . . 10 class x
8		c1st 6133	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5212	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2148	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1352	. . . . . . . . 9 class s
13	3	cv 1352	. . . . . . . . . 10 class y
14	13, 8	cfv 5212	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2148	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1352	. . . . . . . . 9 class q
18		cmq 7273	. . . . . . . . . 10 class .Q
19	6, 12, 18	co 5869	. . . . . . . . 9 class ( r .Q s )
20	17, 19	wceq 1353	. . . . . . . 8 wff q = ( r .Q s )
21	10, 15, 20	w3a 978	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
22		cnq 7270	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2456	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
24	23, 5, 22	wrex 2456	. . . . 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 2459	. . . 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 6134	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5212	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2148	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5212	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2148	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 978	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
32	31, 11, 22	wrex 2456	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
33	32, 5, 22	wrex 2456	. . . . 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 2459	. . . 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 3594	. . 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 5871	. 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 1353	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  7529  dmmp  7531  mulnqprl  7558  mulnqpru  7559  mulclpr  7562  mulnqprlemrl  7563  mulnqprlemru  7564  mulassprg  7571  distrlem1prl  7572  distrlem1pru  7573  distrlem4prl  7574  distrlem4pru  7575  distrlem5prl  7576  distrlem5pru  7577  1idprl  7580  1idpru  7581  recexprlem1ssl  7623  recexprlem1ssu  7624  recexprlemss1l  7625  recexprlemss1u  7626