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 .P. ( B +P. C ) ) = ( ( A .P. B ) +P. ( A .P. C ) )

Proof

Step Hyp Ref Expression
1 distrlem1pr 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( A .P. ( B +P. C ) ) C_ ( ( A .P. B ) +P. ( A .P. C ) ) )
2 distrlem5pr 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( A .P. B ) +P. ( A .P. C ) ) C_ ( A .P. ( B +P. C ) ) )
3 1 2 eqssd 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( A .P. ( B +P. C ) ) = ( ( A .P. B ) +P. ( A .P. C ) ) )
4 dmplp 
 |-  dom +P. = ( P. X. P. )
5 0npr 
 |-  -. (/) e. P.
6 dmmp 
 |-  dom .P. = ( P. X. P. )
7 4 5 6 ndmovdistr 
 |-  ( -. ( A e. P. /\ B e. P. /\ C e. P. ) -> ( A .P. ( B +P. C ) ) = ( ( A .P. B ) +P. ( A .P. C ) ) )
8 3 7 pm2.61i 
 |-  ( A .P. ( B +P. C ) ) = ( ( A .P. B ) +P. ( A .P. C ) )