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 +P = ( 𝑥P , 𝑦P ↦ { 𝑤 ∣ ∃ 𝑣𝑥𝑢𝑦 𝑤 = ( 𝑣 +Q 𝑢 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpp +P
1 vx 𝑥
2 cnp P
3 vy 𝑦
4 vw 𝑤
5 vv 𝑣
6 1 cv 𝑥
7 vu 𝑢
8 3 cv 𝑦
9 4 cv 𝑤
10 5 cv 𝑣
11 cplq +Q
12 7 cv 𝑢
13 10 12 11 co ( 𝑣 +Q 𝑢 )
14 9 13 wceq 𝑤 = ( 𝑣 +Q 𝑢 )
15 14 7 8 wrex 𝑢𝑦 𝑤 = ( 𝑣 +Q 𝑢 )
16 15 5 6 wrex 𝑣𝑥𝑢𝑦 𝑤 = ( 𝑣 +Q 𝑢 )
17 16 4 cab { 𝑤 ∣ ∃ 𝑣𝑥𝑢𝑦 𝑤 = ( 𝑣 +Q 𝑢 ) }
18 1 3 2 2 17 cmpo ( 𝑥P , 𝑦P ↦ { 𝑤 ∣ ∃ 𝑣𝑥𝑢𝑦 𝑤 = ( 𝑣 +Q 𝑢 ) } )
19 0 18 wceq +P = ( 𝑥P , 𝑦P ↦ { 𝑤 ∣ ∃ 𝑣𝑥𝑢𝑦 𝑤 = ( 𝑣 +Q 𝑢 ) } )