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

Definition df-iplp 6623
Description: Define addition on positive reals. From Section 11.2.1 of [HoTT], p. (varies). We write this definition to closely resemble the definition in HoTT although some of the conditions are redundant (for example,  r  e.  ( 1st `  x ) implies 
r  e.  Q.) and can be simplified as shown at genpdf 6663.

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, 26-Sep-2019.)

Assertion
Ref Expression
df-iplp  |-  +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-iplp
StepHypRef Expression
1 cpp 6448 . 2  class  +P.
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cnp 6446 . . 3  class  P.
5 vr . . . . . . . . . 10  setvar  r
65cv 1258 . . . . . . . . 9  class  r
72cv 1258 . . . . . . . . . 10  class  x
8 c1st 5792 . . . . . . . . . 10  class  1st
97, 8cfv 4929 . . . . . . . . 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 4929 . . . . . . . . 9  class  ( 1st `  y )
1512, 14wcel 1409 . . . . . . . 8  wff  s  e.  ( 1st `  y
)
16 vq . . . . . . . . . 10  setvar  q
1716cv 1258 . . . . . . . . 9  class  q
18 cplq 6437 . . . . . . . . . 10  class  +Q
196, 12, 18co 5539 . . . . . . . . 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 6435 . . . . . . 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 5793 . . . . . . . . . 10  class  2nd
277, 26cfv 4929 . . . . . . . . 9  class  ( 2nd `  x )
286, 27wcel 1409 . . . . . . . 8  wff  r  e.  ( 2nd `  x
)
2913, 26cfv 4929 . . . . . . . . 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 3405 . . 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 5541 . 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:  addnqprl  6684  addnqpru  6685  addclpr  6692  plpvlu  6693  dmplp  6695  addnqprlemrl  6712  addnqprlemru  6713  addassprg  6734  distrlem1prl  6737  distrlem1pru  6738  distrlem4prl  6739  distrlem4pru  6740  distrlem5prl  6741  distrlem5pru  6742  ltaddpr  6752  ltexprlemfl  6764  ltexprlemrl  6765  ltexprlemfu  6766  ltexprlemru  6767  addcanprleml  6769  addcanprlemu  6770  cauappcvgprlemladdfu  6809  cauappcvgprlemladdfl  6810  caucvgprlemladdfu  6832
  Copyright terms: Public domain W3C validator