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

Definition df-iplp 7498
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 7538.

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 7323 . 2  class  +P.
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cnp 7321 . . 3  class  P.
5 vr . . . . . . . . . 10  setvar  r
65cv 1363 . . . . . . . . 9  class  r
72cv 1363 . . . . . . . . . 10  class  x
8 c1st 6164 . . . . . . . . . 10  class  1st
97, 8cfv 5235 . . . . . . . . 9  class  ( 1st `  x )
106, 9wcel 2160 . . . . . . . 8  wff  r  e.  ( 1st `  x
)
11 vs . . . . . . . . . 10  setvar  s
1211cv 1363 . . . . . . . . 9  class  s
133cv 1363 . . . . . . . . . 10  class  y
1413, 8cfv 5235 . . . . . . . . 9  class  ( 1st `  y )
1512, 14wcel 2160 . . . . . . . 8  wff  s  e.  ( 1st `  y
)
16 vq . . . . . . . . . 10  setvar  q
1716cv 1363 . . . . . . . . 9  class  q
18 cplq 7312 . . . . . . . . . 10  class  +Q
196, 12, 18co 5897 . . . . . . . . 9  class  ( r  +Q  s )
2017, 19wceq 1364 . . . . . . . 8  wff  q  =  ( r  +Q  s
)
2110, 15, 20w3a 980 . . . . . . 7  wff  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  +Q  s ) )
22 cnq 7310 . . . . . . 7  class  Q.
2321, 11, 22wrex 2469 . . . . . 6  wff  E. s  e.  Q.  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  +Q  s ) )
2423, 5, 22wrex 2469 . . . . 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 2472 . . . 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 6165 . . . . . . . . . 10  class  2nd
277, 26cfv 5235 . . . . . . . . 9  class  ( 2nd `  x )
286, 27wcel 2160 . . . . . . . 8  wff  r  e.  ( 2nd `  x
)
2913, 26cfv 5235 . . . . . . . . 9  class  ( 2nd `  y )
3012, 29wcel 2160 . . . . . . . 8  wff  s  e.  ( 2nd `  y
)
3128, 30, 20w3a 980 . . . . . . 7  wff  ( r  e.  ( 2nd `  x
)  /\  s  e.  ( 2nd `  y )  /\  q  =  ( r  +Q  s ) )
3231, 11, 22wrex 2469 . . . . . 6  wff  E. s  e.  Q.  ( r  e.  ( 2nd `  x
)  /\  s  e.  ( 2nd `  y )  /\  q  =  ( r  +Q  s ) )
3332, 5, 22wrex 2469 . . . . 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 2472 . . . 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 3610 . . 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 5899 . 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 1364 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  7559  addnqpru  7560  addclpr  7567  plpvlu  7568  dmplp  7570  addnqprlemrl  7587  addnqprlemru  7588  addassprg  7609  distrlem1prl  7612  distrlem1pru  7613  distrlem4prl  7614  distrlem4pru  7615  distrlem5prl  7616  distrlem5pru  7617  ltaddpr  7627  ltexprlemfl  7639  ltexprlemrl  7640  ltexprlemfu  7641  ltexprlemru  7642  addcanprleml  7644  addcanprlemu  7645  cauappcvgprlemladdfu  7684  cauappcvgprlemladdfl  7685  caucvgprlemladdfu  7707
  Copyright terms: Public domain W3C validator