Theorem plpv

Description: Value of addition on positive reals. (Contributed by NM, 28-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	plpv	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 +P 𝐵 ) = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 +Q 𝑧 ) } )

Proof

Step	Hyp	Ref	Expression
1		df-plp	⊢ +P = ( 𝑢 ∈ P , 𝑣 ∈ P ↦ { 𝑓 ∣ ∃ 𝑔 ∈ 𝑢 ∃ ℎ ∈ 𝑣 𝑓 = ( 𝑔 +Q ℎ ) } )
2		addclnq	⊢ ( ( 𝑔 ∈ Q ∧ ℎ ∈ Q ) → ( 𝑔 +Q ℎ ) ∈ Q )
3	1 2	genpv	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 +P 𝐵 ) = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 +Q 𝑧 ) } )