Theorem mpv

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

	Ref	Expression
Assertion	mpv	$$⊢\left(A\in 𝑷\wedge B\in 𝑷\right)\to A{\cdot }_{𝑷}B=\left\{x|\exists y\in A\exists z\in Bx=y{\cdot }_{𝑸}z\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-mp	$$⊢{\cdot }_{𝑷}=\left(u\in 𝑷,v\in 𝑷⟼\left\{f|\exists g\in u\exists h\in vf=g{\cdot }_{𝑸}h\right\}\right)$$
2		mulclnq	$$⊢\left(g\in 𝑸\wedge h\in 𝑸\right)\to g{\cdot }_{𝑸}h\in 𝑸$$
3	1 2	genpv	$$⊢\left(A\in 𝑷\wedge B\in 𝑷\right)\to A{\cdot }_{𝑷}B=\left\{x|\exists y\in A\exists z\in Bx=y{\cdot }_{𝑸}z\right\}$$