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{\cdot }_{𝑷}\left(B{+}_{𝑷}C\right)=\left(A{\cdot }_{𝑷}B\right){+}_{𝑷}\left(A{\cdot }_{𝑷}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		distrlem1pr	$$⊢\left(A\in 𝑷\wedge B\in 𝑷\wedge C\in 𝑷\right)\to A{\cdot }_{𝑷}\left(B{+}_{𝑷}C\right)\subseteq \left(A{\cdot }_{𝑷}B\right){+}_{𝑷}\left(A{\cdot }_{𝑷}C\right)$$
2		distrlem5pr	$$⊢\left(A\in 𝑷\wedge B\in 𝑷\wedge C\in 𝑷\right)\to \left(A{\cdot }_{𝑷}B\right){+}_{𝑷}\left(A{\cdot }_{𝑷}C\right)\subseteq A{\cdot }_{𝑷}\left(B{+}_{𝑷}C\right)$$
3	1 2	eqssd	$$⊢\left(A\in 𝑷\wedge B\in 𝑷\wedge C\in 𝑷\right)\to A{\cdot }_{𝑷}\left(B{+}_{𝑷}C\right)=\left(A{\cdot }_{𝑷}B\right){+}_{𝑷}\left(A{\cdot }_{𝑷}C\right)$$
4		dmplp	$$⊢\mathrm{dom}{+}_{𝑷}=𝑷\times 𝑷$$
5		0npr	$$⊢\neg \varnothing \in 𝑷$$
6		dmmp	$$⊢\mathrm{dom}{\cdot }_{𝑷}=𝑷\times 𝑷$$
7	4 5 6	ndmovdistr	$$⊢\neg \left(A\in 𝑷\wedge B\in 𝑷\wedge C\in 𝑷\right)\to A{\cdot }_{𝑷}\left(B{+}_{𝑷}C\right)=\left(A{\cdot }_{𝑷}B\right){+}_{𝑷}\left(A{\cdot }_{𝑷}C\right)$$
8	3 7	pm2.61i	$$⊢A{\cdot }_{𝑷}\left(B{+}_{𝑷}C\right)=\left(A{\cdot }_{𝑷}B\right){+}_{𝑷}\left(A{\cdot }_{𝑷}C\right)$$