ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-imp Unicode version

Definition df-imp 7481
Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7480 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
StepHypRef Expression
1 cmp 7306 . 2  class  .P.
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cnp 7303 . . 3  class  P.
5 vr . . . . . . . . . 10  setvar  r
65cv 1362 . . . . . . . . 9  class  r
72cv 1362 . . . . . . . . . 10  class  x
8 c1st 6152 . . . . . . . . . 10  class  1st
97, 8cfv 5228 . . . . . . . . 9  class  ( 1st `  x )
106, 9wcel 2158 . . . . . . . 8  wff  r  e.  ( 1st `  x
)
11 vs . . . . . . . . . 10  setvar  s
1211cv 1362 . . . . . . . . 9  class  s
133cv 1362 . . . . . . . . . 10  class  y
1413, 8cfv 5228 . . . . . . . . 9  class  ( 1st `  y )
1512, 14wcel 2158 . . . . . . . 8  wff  s  e.  ( 1st `  y
)
16 vq . . . . . . . . . 10  setvar  q
1716cv 1362 . . . . . . . . 9  class  q
18 cmq 7295 . . . . . . . . . 10  class  .Q
196, 12, 18co 5888 . . . . . . . . 9  class  ( r  .Q  s )
2017, 19wceq 1363 . . . . . . . 8  wff  q  =  ( r  .Q  s
)
2110, 15, 20w3a 979 . . . . . . 7  wff  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  .Q  s ) )
22 cnq 7292 . . . . . . 7  class  Q.
2321, 11, 22wrex 2466 . . . . . 6  wff  E. s  e.  Q.  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  .Q  s ) )
2423, 5, 22wrex 2466 . . . . 5  wff  E. r  e.  Q.  E. s  e. 
Q.  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  .Q  s ) )
2524, 16, 22crab 2469 . . . 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 6153 . . . . . . . . . 10  class  2nd
277, 26cfv 5228 . . . . . . . . 9  class  ( 2nd `  x )
286, 27wcel 2158 . . . . . . . 8  wff  r  e.  ( 2nd `  x
)
2913, 26cfv 5228 . . . . . . . . 9  class  ( 2nd `  y )
3012, 29wcel 2158 . . . . . . . 8  wff  s  e.  ( 2nd `  y
)
3128, 30, 20w3a 979 . . . . . . 7  wff  ( r  e.  ( 2nd `  x
)  /\  s  e.  ( 2nd `  y )  /\  q  =  ( r  .Q  s ) )
3231, 11, 22wrex 2466 . . . . . 6  wff  E. s  e.  Q.  ( r  e.  ( 2nd `  x
)  /\  s  e.  ( 2nd `  y )  /\  q  =  ( r  .Q  s ) )
3332, 5, 22wrex 2466 . . . . 5  wff  E. r  e.  Q.  E. s  e. 
Q.  ( r  e.  ( 2nd `  x
)  /\  s  e.  ( 2nd `  y )  /\  q  =  ( r  .Q  s ) )
3433, 16, 22crab 2469 . . . 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 ) ) }
3525, 34cop 3607 . . 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
) ) } >.
362, 3, 4, 4, 35cmpo 5890 . 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
) ) } >. )
371, 36wceq 1363 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
) ) } >. )
Colors of variables: wff set class
This definition is referenced by:  mpvlu  7551  dmmp  7553  mulnqprl  7580  mulnqpru  7581  mulclpr  7584  mulnqprlemrl  7585  mulnqprlemru  7586  mulassprg  7593  distrlem1prl  7594  distrlem1pru  7595  distrlem4prl  7596  distrlem4pru  7597  distrlem5prl  7598  distrlem5pru  7599  1idprl  7602  1idpru  7603  recexprlem1ssl  7645  recexprlem1ssu  7646  recexprlemss1l  7647  recexprlemss1u  7648
  Copyright terms: Public domain W3C validator