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

Definition df-imp 6625
Description: Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 6624 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 6450 . 2  class  .P.
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cnp 6447 . . 3  class  P.
5 vr . . . . . . . . . 10  setvar  r
65cv 1258 . . . . . . . . 9  class  r
72cv 1258 . . . . . . . . . 10  class  x
8 c1st 5793 . . . . . . . . . 10  class  1st
97, 8cfv 4930 . . . . . . . . 9  class  ( 1st `  x )
106, 9wcel 1409 . . . . . . . 8  wff  r  e.  ( 1st `  x
)
11 vs . . . . . . . . . 10  setvar  s
1211cv 1258 . . . . . . . . 9  class  s
133cv 1258 . . . . . . . . . 10  class  y
1413, 8cfv 4930 . . . . . . . . 9  class  ( 1st `  y )
1512, 14wcel 1409 . . . . . . . 8  wff  s  e.  ( 1st `  y
)
16 vq . . . . . . . . . 10  setvar  q
1716cv 1258 . . . . . . . . 9  class  q
18 cmq 6439 . . . . . . . . . 10  class  .Q
196, 12, 18co 5540 . . . . . . . . 9  class  ( r  .Q  s )
2017, 19wceq 1259 . . . . . . . 8  wff  q  =  ( r  .Q  s
)
2110, 15, 20w3a 896 . . . . . . 7  wff  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  .Q  s ) )
22 cnq 6436 . . . . . . 7  class  Q.
2321, 11, 22wrex 2324 . . . . . 6  wff  E. s  e.  Q.  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  .Q  s ) )
2423, 5, 22wrex 2324 . . . . 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 2327 . . . 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 5794 . . . . . . . . . 10  class  2nd
277, 26cfv 4930 . . . . . . . . 9  class  ( 2nd `  x )
286, 27wcel 1409 . . . . . . . 8  wff  r  e.  ( 2nd `  x
)
2913, 26cfv 4930 . . . . . . . . 9  class  ( 2nd `  y )
3012, 29wcel 1409 . . . . . . . 8  wff  s  e.  ( 2nd `  y
)
3128, 30, 20w3a 896 . . . . . . 7  wff  ( r  e.  ( 2nd `  x
)  /\  s  e.  ( 2nd `  y )  /\  q  =  ( r  .Q  s ) )
3231, 11, 22wrex 2324 . . . . . 6  wff  E. s  e.  Q.  ( r  e.  ( 2nd `  x
)  /\  s  e.  ( 2nd `  y )  /\  q  =  ( r  .Q  s ) )
3332, 5, 22wrex 2324 . . . . 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 2327 . . . 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 3406 . . 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 5542 . 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 1259 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  6695  dmmp  6697  mulnqprl  6724  mulnqpru  6725  mulclpr  6728  mulnqprlemrl  6729  mulnqprlemru  6730  mulassprg  6737  distrlem1prl  6738  distrlem1pru  6739  distrlem4prl  6740  distrlem4pru  6741  distrlem5prl  6742  distrlem5pru  6743  1idprl  6746  1idpru  6747  recexprlem1ssl  6789  recexprlem1ssu  6790  recexprlemss1l  6791  recexprlemss1u  6792
  Copyright terms: Public domain W3C validator