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