Theorem dmmp

Description: Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	dmmp	⊢ dom ·P = ( P × P )

Proof

Step	Hyp	Ref	Expression
1		df-mp	⊢ ·P = ( 𝑥 ∈ P , 𝑦 ∈ P ↦ { 𝑧 ∣ ∃ 𝑢 ∈ 𝑥 ∃ 𝑣 ∈ 𝑦 𝑧 = ( 𝑢 ·Q 𝑣 ) } )
2		mulclnq	⊢ ( ( 𝑢 ∈ Q ∧ 𝑣 ∈ Q ) → ( 𝑢 ·Q 𝑣 ) ∈ Q )
3	1 2	genpdm	⊢ dom ·P = ( P × P )