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 ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) = ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) )

Proof

Step Hyp Ref Expression
1 distrlem1pr ( ( 𝐴P𝐵P𝐶P ) → ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ⊆ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) )
2 distrlem5pr ( ( 𝐴P𝐵P𝐶P ) → ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) ⊆ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) )
3 1 2 eqssd ( ( 𝐴P𝐵P𝐶P ) → ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) = ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) )
4 dmplp dom +P = ( P × P )
5 0npr ¬ ∅ ∈ P
6 dmmp dom ·P = ( P × P )
7 4 5 6 ndmovdistr ( ¬ ( 𝐴P𝐵P𝐶P ) → ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) = ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) )
8 3 7 pm2.61i ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) = ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) )