Metamath Proof Explorer

Theorem distrpr

Description: Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of Gleason p. 124. (Contributed by NM, 2-May-1996) (New usage is discouraged.)

Ref Expression
Assertion distrpr ⊢ A ⋅ 𝑷 B + 𝑷 C = A ⋅ 𝑷 B + 𝑷 A ⋅ 𝑷 C

Proof

Step Hyp Ref Expression
1 distrlem1pr ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → A ⋅ 𝑷 B + 𝑷 C ⊆ A ⋅ 𝑷 B + 𝑷 A ⋅ 𝑷 C
2 distrlem5pr ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → A ⋅ 𝑷 B + 𝑷 A ⋅ 𝑷 C ⊆ A ⋅ 𝑷 B + 𝑷 C
3 1 2 eqssd ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → A ⋅ 𝑷 B + 𝑷 C = A ⋅ 𝑷 B + 𝑷 A ⋅ 𝑷 C
4 dmplp ⊢ dom ⁡ + 𝑷 = 𝑷 × 𝑷
5 0npr ⊢ ¬ ∅ ∈ 𝑷
6 dmmp ⊢ dom ⁡ ⋅ 𝑷 = 𝑷 × 𝑷
7 4 5 6 ndmovdistr ⊢ ¬ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → A ⋅ 𝑷 B + 𝑷 C = A ⋅ 𝑷 B + 𝑷 A ⋅ 𝑷 C
8 3 7 pm2.61i ⊢ A ⋅ 𝑷 B + 𝑷 C = A ⋅ 𝑷 B + 𝑷 A ⋅ 𝑷 C