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

Definition df-iplp 6797
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 6837.

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 6622 . 2  class  +P.
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cnp 6620 . . 3  class  P.
5 vr . . . . . . . . . 10  setvar  r
65cv 1284 . . . . . . . . 9  class  r
72cv 1284 . . . . . . . . . 10  class  x
8 c1st 5818 . . . . . . . . . 10  class  1st
97, 8cfv 4953 . . . . . . . . 9  class  ( 1st `  x )
106, 9wcel 1434 . . . . . . . 8  wff  r  e.  ( 1st `  x
)
11 vs . . . . . . . . . 10  setvar  s
1211cv 1284 . . . . . . . . 9  class  s
133cv 1284 . . . . . . . . . 10  class  y
1413, 8cfv 4953 . . . . . . . . 9  class  ( 1st `  y )
1512, 14wcel 1434 . . . . . . . 8  wff  s  e.  ( 1st `  y
)
16 vq . . . . . . . . . 10  setvar  q
1716cv 1284 . . . . . . . . 9  class  q
18 cplq 6611 . . . . . . . . . 10  class  +Q
196, 12, 18co 5565 . . . . . . . . 9  class  ( r  +Q  s )
2017, 19wceq 1285 . . . . . . . 8  wff  q  =  ( r  +Q  s
)
2110, 15, 20w3a 920 . . . . . . 7  wff  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  +Q  s ) )
22 cnq 6609 . . . . . . 7  class  Q.
2321, 11, 22wrex 2354 . . . . . 6  wff  E. s  e.  Q.  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  +Q  s ) )
2423, 5, 22wrex 2354 . . . . 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 2357 . . . 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 5819 . . . . . . . . . 10  class  2nd
277, 26cfv 4953 . . . . . . . . 9  class  ( 2nd `  x )
286, 27wcel 1434 . . . . . . . 8  wff  r  e.  ( 2nd `  x
)
2913, 26cfv 4953 . . . . . . . . 9  class  ( 2nd `  y )
3012, 29wcel 1434 . . . . . . . 8  wff  s  e.  ( 2nd `  y
)
3128, 30, 20w3a 920 . . . . . . 7  wff  ( r  e.  ( 2nd `  x
)  /\  s  e.  ( 2nd `  y )  /\  q  =  ( r  +Q  s ) )
3231, 11, 22wrex 2354 . . . . . 6  wff  E. s  e.  Q.  ( r  e.  ( 2nd `  x
)  /\  s  e.  ( 2nd `  y )  /\  q  =  ( r  +Q  s ) )
3332, 5, 22wrex 2354 . . . . 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 2357 . . . 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 3420 . . 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 5567 . 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 1285 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  6858  addnqpru  6859  addclpr  6866  plpvlu  6867  dmplp  6869  addnqprlemrl  6886  addnqprlemru  6887  addassprg  6908  distrlem1prl  6911  distrlem1pru  6912  distrlem4prl  6913  distrlem4pru  6914  distrlem5prl  6915  distrlem5pru  6916  ltaddpr  6926  ltexprlemfl  6938  ltexprlemrl  6939  ltexprlemfu  6940  ltexprlemru  6941  addcanprleml  6943  addcanprlemu  6944  cauappcvgprlemladdfu  6983  cauappcvgprlemladdfl  6984  caucvgprlemladdfu  7006
  Copyright terms: Public domain W3C validator