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

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 𝐶 ) )