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