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

Definition df-imp 7089
Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7088 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 6914 . 2  class  .P.
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cnp 6911 . . 3  class  P.
5 vr . . . . . . . . . 10  setvar  r
65cv 1289 . . . . . . . . 9  class  r
72cv 1289 . . . . . . . . . 10  class  x
8 c1st 5923 . . . . . . . . . 10  class  1st
97, 8cfv 5028 . . . . . . . . 9  class  ( 1st `  x )
106, 9wcel 1439 . . . . . . . 8  wff  r  e.  ( 1st `  x
)
11 vs . . . . . . . . . 10  setvar  s
1211cv 1289 . . . . . . . . 9  class  s
133cv 1289 . . . . . . . . . 10  class  y
1413, 8cfv 5028 . . . . . . . . 9  class  ( 1st `  y )
1512, 14wcel 1439 . . . . . . . 8  wff  s  e.  ( 1st `  y
)
16 vq . . . . . . . . . 10  setvar  q
1716cv 1289 . . . . . . . . 9  class  q
18 cmq 6903 . . . . . . . . . 10  class  .Q
196, 12, 18co 5666 . . . . . . . . 9  class  ( r  .Q  s )
2017, 19wceq 1290 . . . . . . . 8  wff  q  =  ( r  .Q  s
)
2110, 15, 20w3a 925 . . . . . . 7  wff  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  .Q  s ) )
22 cnq 6900 . . . . . . 7  class  Q.
2321, 11, 22wrex 2361 . . . . . 6  wff  E. s  e.  Q.  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  .Q  s ) )
2423, 5, 22wrex 2361 . . . . 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 2364 . . . 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 5924 . . . . . . . . . 10  class  2nd
277, 26cfv 5028 . . . . . . . . 9  class  ( 2nd `  x )
286, 27wcel 1439 . . . . . . . 8  wff  r  e.  ( 2nd `  x
)
2913, 26cfv 5028 . . . . . . . . 9  class  ( 2nd `  y )
3012, 29wcel 1439 . . . . . . . 8  wff  s  e.  ( 2nd `  y
)
3128, 30, 20w3a 925 . . . . . . 7  wff  ( r  e.  ( 2nd `  x
)  /\  s  e.  ( 2nd `  y )  /\  q  =  ( r  .Q  s ) )
3231, 11, 22wrex 2361 . . . . . 6  wff  E. s  e.  Q.  ( r  e.  ( 2nd `  x
)  /\  s  e.  ( 2nd `  y )  /\  q  =  ( r  .Q  s ) )
3332, 5, 22wrex 2361 . . . . 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 2364 . . . 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 3453 . . 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, 35cmpt2 5668 . 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 1290 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  7159  dmmp  7161  mulnqprl  7188  mulnqpru  7189  mulclpr  7192  mulnqprlemrl  7193  mulnqprlemru  7194  mulassprg  7201  distrlem1prl  7202  distrlem1pru  7203  distrlem4prl  7204  distrlem4pru  7205  distrlem5prl  7206  distrlem5pru  7207  1idprl  7210  1idpru  7211  recexprlem1ssl  7253  recexprlem1ssu  7254  recexprlemss1l  7255  recexprlemss1u  7256
  Copyright terms: Public domain W3C validator