Metamath Proof Explorer

Definition df-plr

Description: Define addition on signed reals. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-4.3 of Gleason p. 126. (Contributed by NM, 25-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion df-plr 
|- +R = { <. <. x , y >. , z >. | ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cplr 
 |-  +R
1 vx 
 |-  x
2 vy 
 |-  y
3 vz 
 |-  z
4 1 cv 
 |-  x
5 cnr 
 |-  R.
6 4 5 wcel 
 |-  x e. R.
7 2 cv 
 |-  y
8 7 5 wcel 
 |-  y e. R.
9 6 8 wa 
 |-  ( x e. R. /\ y e. R. )
10 vw 
 |-  w
11 vv 
 |-  v
12 vu 
 |-  u
13 vf 
 |-  f
14 10 cv 
 |-  w
15 11 cv 
 |-  v
16 14 15 cop 
 |-  <. w , v >.
17 cer 
 |-  ~R
18 16 17 cec 
 |-  [ <. w , v >. ] ~R
19 4 18 wceq 
 |-  x = [ <. w , v >. ] ~R
20 12 cv 
 |-  u
21 13 cv 
 |-  f
22 20 21 cop 
 |-  <. u , f >.
23 22 17 cec 
 |-  [ <. u , f >. ] ~R
24 7 23 wceq 
 |-  y = [ <. u , f >. ] ~R
25 19 24 wa 
 |-  ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R )
26 3 cv 
 |-  z
27 cpp 
 |-  +P.
28 14 20 27 co 
 |-  ( w +P. u )
29 15 21 27 co 
 |-  ( v +P. f )
30 28 29 cop 
 |-  <. ( w +P. u ) , ( v +P. f ) >.
31 30 17 cec 
 |-  [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R
32 26 31 wceq 
 |-  z = [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R
33 25 32 wa 
 |-  ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R )
34 33 13 wex 
 |-  E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R )
35 34 12 wex 
 |-  E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R )
36 35 11 wex 
 |-  E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R )
37 36 10 wex 
 |-  E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R )
38 9 37 wa 
 |-  ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R ) )
39 38 1 2 3 coprab 
 |-  { <. <. x , y >. , z >. | ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R ) ) }
40 0 39 wceq 
 |-  +R = { <. <. x , y >. , z >. | ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R ) ) }