Theorem mpv

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

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

Proof

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