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

Definition df-iplp 7177
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 7217.

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 7002 . 2  class  +P.
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cnp 7000 . . 3  class  P.
5 vr . . . . . . . . . 10  setvar  r
65cv 1298 . . . . . . . . 9  class  r
72cv 1298 . . . . . . . . . 10  class  x
8 c1st 5967 . . . . . . . . . 10  class  1st
97, 8cfv 5059 . . . . . . . . 9  class  ( 1st `  x )
106, 9wcel 1448 . . . . . . . 8  wff  r  e.  ( 1st `  x
)
11 vs . . . . . . . . . 10  setvar  s
1211cv 1298 . . . . . . . . 9  class  s
133cv 1298 . . . . . . . . . 10  class  y
1413, 8cfv 5059 . . . . . . . . 9  class  ( 1st `  y )
1512, 14wcel 1448 . . . . . . . 8  wff  s  e.  ( 1st `  y
)
16 vq . . . . . . . . . 10  setvar  q
1716cv 1298 . . . . . . . . 9  class  q
18 cplq 6991 . . . . . . . . . 10  class  +Q
196, 12, 18co 5706 . . . . . . . . 9  class  ( r  +Q  s )
2017, 19wceq 1299 . . . . . . . 8  wff  q  =  ( r  +Q  s
)
2110, 15, 20w3a 930 . . . . . . 7  wff  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  +Q  s ) )
22 cnq 6989 . . . . . . 7  class  Q.
2321, 11, 22wrex 2376 . . . . . 6  wff  E. s  e.  Q.  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  +Q  s ) )
2423, 5, 22wrex 2376 . . . . 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 2379 . . . 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 5968 . . . . . . . . . 10  class  2nd
277, 26cfv 5059 . . . . . . . . 9  class  ( 2nd `  x )
286, 27wcel 1448 . . . . . . . 8  wff  r  e.  ( 2nd `  x
)
2913, 26cfv 5059 . . . . . . . . 9  class  ( 2nd `  y )
3012, 29wcel 1448 . . . . . . . 8  wff  s  e.  ( 2nd `  y
)
3128, 30, 20w3a 930 . . . . . . 7  wff  ( r  e.  ( 2nd `  x
)  /\  s  e.  ( 2nd `  y )  /\  q  =  ( r  +Q  s ) )
3231, 11, 22wrex 2376 . . . . . 6  wff  E. s  e.  Q.  ( r  e.  ( 2nd `  x
)  /\  s  e.  ( 2nd `  y )  /\  q  =  ( r  +Q  s ) )
3332, 5, 22wrex 2376 . . . . 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 2379 . . . 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 3477 . . 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 5708 . 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 1299 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  7238  addnqpru  7239  addclpr  7246  plpvlu  7247  dmplp  7249  addnqprlemrl  7266  addnqprlemru  7267  addassprg  7288  distrlem1prl  7291  distrlem1pru  7292  distrlem4prl  7293  distrlem4pru  7294  distrlem5prl  7295  distrlem5pru  7296  ltaddpr  7306  ltexprlemfl  7318  ltexprlemrl  7319  ltexprlemfu  7320  ltexprlemru  7321  addcanprleml  7323  addcanprlemu  7324  cauappcvgprlemladdfu  7363  cauappcvgprlemladdfl  7364  caucvgprlemladdfu  7386
  Copyright terms: Public domain W3C validator