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

Definition df-iplp 6971
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 7011.

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 6796 . 2  class  +P.
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cnp 6794 . . 3  class  P.
5 vr . . . . . . . . . 10  setvar  r
65cv 1286 . . . . . . . . 9  class  r
72cv 1286 . . . . . . . . . 10  class  x
8 c1st 5866 . . . . . . . . . 10  class  1st
97, 8cfv 4981 . . . . . . . . 9  class  ( 1st `  x )
106, 9wcel 1436 . . . . . . . 8  wff  r  e.  ( 1st `  x
)
11 vs . . . . . . . . . 10  setvar  s
1211cv 1286 . . . . . . . . 9  class  s
133cv 1286 . . . . . . . . . 10  class  y
1413, 8cfv 4981 . . . . . . . . 9  class  ( 1st `  y )
1512, 14wcel 1436 . . . . . . . 8  wff  s  e.  ( 1st `  y
)
16 vq . . . . . . . . . 10  setvar  q
1716cv 1286 . . . . . . . . 9  class  q
18 cplq 6785 . . . . . . . . . 10  class  +Q
196, 12, 18co 5613 . . . . . . . . 9  class  ( r  +Q  s )
2017, 19wceq 1287 . . . . . . . 8  wff  q  =  ( r  +Q  s
)
2110, 15, 20w3a 922 . . . . . . 7  wff  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  +Q  s ) )
22 cnq 6783 . . . . . . 7  class  Q.
2321, 11, 22wrex 2356 . . . . . 6  wff  E. s  e.  Q.  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  +Q  s ) )
2423, 5, 22wrex 2356 . . . . 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 2359 . . . 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 5867 . . . . . . . . . 10  class  2nd
277, 26cfv 4981 . . . . . . . . 9  class  ( 2nd `  x )
286, 27wcel 1436 . . . . . . . 8  wff  r  e.  ( 2nd `  x
)
2913, 26cfv 4981 . . . . . . . . 9  class  ( 2nd `  y )
3012, 29wcel 1436 . . . . . . . 8  wff  s  e.  ( 2nd `  y
)
3128, 30, 20w3a 922 . . . . . . 7  wff  ( r  e.  ( 2nd `  x
)  /\  s  e.  ( 2nd `  y )  /\  q  =  ( r  +Q  s ) )
3231, 11, 22wrex 2356 . . . . . 6  wff  E. s  e.  Q.  ( r  e.  ( 2nd `  x
)  /\  s  e.  ( 2nd `  y )  /\  q  =  ( r  +Q  s ) )
3332, 5, 22wrex 2356 . . . . 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 2359 . . . 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 3434 . . 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 5615 . 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 1287 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  7032  addnqpru  7033  addclpr  7040  plpvlu  7041  dmplp  7043  addnqprlemrl  7060  addnqprlemru  7061  addassprg  7082  distrlem1prl  7085  distrlem1pru  7086  distrlem4prl  7087  distrlem4pru  7088  distrlem5prl  7089  distrlem5pru  7090  ltaddpr  7100  ltexprlemfl  7112  ltexprlemrl  7113  ltexprlemfu  7114  ltexprlemru  7115  addcanprleml  7117  addcanprlemu  7118  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  caucvgprlemladdfu  7180
  Copyright terms: Public domain W3C validator