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