Definition df-imp 7435

Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7434 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 7260	. 2 class .P.
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cnp 7257	. . 3 class P.
5		vr	. . . . . . . . . 10 setvar r
6	5	cv 1348	. . . . . . . . 9 class r
7	2	cv 1348	. . . . . . . . . 10 class x
8		c1st 6121	. . . . . . . . . 10 class 1st
9	7, 8	cfv 5200	. . . . . . . . 9 class ( 1st ` x )
10	6, 9	wcel 2142	. . . . . . . 8 wff r e. ( 1st ` x )
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1348	. . . . . . . . 9 class s
13	3	cv 1348	. . . . . . . . . 10 class y
14	13, 8	cfv 5200	. . . . . . . . 9 class ( 1st ` y )
15	12, 14	wcel 2142	. . . . . . . 8 wff s e. ( 1st ` y )
16		vq	. . . . . . . . . 10 setvar q
17	16	cv 1348	. . . . . . . . 9 class q
18		cmq 7249	. . . . . . . . . 10 class .Q
19	6, 12, 18	co 5857	. . . . . . . . 9 class ( r .Q s )
20	17, 19	wceq 1349	. . . . . . . 8 wff q = ( r .Q s )
21	10, 15, 20	w3a 974	. . . . . . 7 wff ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
22		cnq 7246	. . . . . . 7 class Q.
23	21, 11, 22	wrex 2450	. . . . . 6 wff E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) )
24	23, 5, 22	wrex 2450	. . . . 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 2453	. . . 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 6122	. . . . . . . . . 10 class 2nd
27	7, 26	cfv 5200	. . . . . . . . 9 class ( 2nd ` x )
28	6, 27	wcel 2142	. . . . . . . 8 wff r e. ( 2nd ` x )
29	13, 26	cfv 5200	. . . . . . . . 9 class ( 2nd ` y )
30	12, 29	wcel 2142	. . . . . . . 8 wff s e. ( 2nd ` y )
31	28, 30, 20	w3a 974	. . . . . . 7 wff ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
32	31, 11, 22	wrex 2450	. . . . . 6 wff E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) )
33	32, 5, 22	wrex 2450	. . . . 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 2453	. . . 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 3587	. . 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 5859	. 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 1349	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  7505  dmmp  7507  mulnqprl  7534  mulnqpru  7535  mulclpr  7538  mulnqprlemrl  7539  mulnqprlemru  7540  mulassprg  7547  distrlem1prl  7548  distrlem1pru  7549  distrlem4prl  7550  distrlem4pru  7551  distrlem5prl  7552  distrlem5pru  7553  1idprl  7556  1idpru  7557  recexprlem1ssl  7599  recexprlem1ssu  7600  recexprlemss1l  7601  recexprlemss1u  7602