This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mpv

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

Ref Expression
Assertion mpv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A ⋅ 𝑷 B = x | ∃ y ∈ A ∃ z ∈ B x = y ⋅ 𝑸 z

Proof

Step Hyp Ref Expression
1 df-mp ⊢ ⋅ 𝑷 = u ∈ 𝑷 , v ∈ 𝑷 ⟼ f | ∃ g ∈ u ∃ h ∈ v f = g ⋅ 𝑸 h
2 mulclnq ⊢ g ∈ 𝑸 ∧ h ∈ 𝑸 → g ⋅ 𝑸 h ∈ 𝑸
3 1 2 genpv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A ⋅ 𝑷 B = x | ∃ y ∈ A ∃ z ∈ B x = y ⋅ 𝑸 z