Metamath Proof Explorer


Definition df-plp

Description: Define addition on positive 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-3.5 of Gleason p. 123. (Contributed by NM, 18-Nov-1995) (New usage is discouraged.)

Ref Expression
Assertion df-plp + 𝑷 = x 𝑷 , y 𝑷 w | v x u y w = v + 𝑸 u

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpp class + 𝑷
1 vx setvar x
2 cnp class 𝑷
3 vy setvar y
4 vw setvar w
5 vv setvar v
6 1 cv setvar x
7 vu setvar u
8 3 cv setvar y
9 4 cv setvar w
10 5 cv setvar v
11 cplq class + 𝑸
12 7 cv setvar u
13 10 12 11 co class v + 𝑸 u
14 9 13 wceq wff w = v + 𝑸 u
15 14 7 8 wrex wff u y w = v + 𝑸 u
16 15 5 6 wrex wff v x u y w = v + 𝑸 u
17 16 4 cab class w | v x u y w = v + 𝑸 u
18 1 3 2 2 17 cmpo class x 𝑷 , y 𝑷 w | v x u y w = v + 𝑸 u
19 0 18 wceq wff + 𝑷 = x 𝑷 , y 𝑷 w | v x u y w = v + 𝑸 u