| Step |
Hyp |
Ref |
Expression |
| 1 |
|
submuladdd.1 |
|- ( ph -> A e. CC ) |
| 2 |
|
submuladdd.2 |
|- ( ph -> B e. CC ) |
| 3 |
|
submuladdd.3 |
|- ( ph -> C e. CC ) |
| 4 |
|
submuladdd.4 |
|- ( ph -> D e. CC ) |
| 5 |
1 2
|
subcld |
|- ( ph -> ( A - B ) e. CC ) |
| 6 |
3 4
|
addcld |
|- ( ph -> ( C + D ) e. CC ) |
| 7 |
5 6
|
mulcomd |
|- ( ph -> ( ( A - B ) x. ( C + D ) ) = ( ( C + D ) x. ( A - B ) ) ) |
| 8 |
|
addmulsub |
|- ( ( ( C e. CC /\ D e. CC ) /\ ( A e. CC /\ B e. CC ) ) -> ( ( C + D ) x. ( A - B ) ) = ( ( ( C x. A ) + ( D x. A ) ) - ( ( C x. B ) + ( D x. B ) ) ) ) |
| 9 |
3 4 1 2 8
|
syl22anc |
|- ( ph -> ( ( C + D ) x. ( A - B ) ) = ( ( ( C x. A ) + ( D x. A ) ) - ( ( C x. B ) + ( D x. B ) ) ) ) |
| 10 |
3 1
|
mulcomd |
|- ( ph -> ( C x. A ) = ( A x. C ) ) |
| 11 |
4 1
|
mulcomd |
|- ( ph -> ( D x. A ) = ( A x. D ) ) |
| 12 |
10 11
|
oveq12d |
|- ( ph -> ( ( C x. A ) + ( D x. A ) ) = ( ( A x. C ) + ( A x. D ) ) ) |
| 13 |
3 2
|
mulcomd |
|- ( ph -> ( C x. B ) = ( B x. C ) ) |
| 14 |
4 2
|
mulcomd |
|- ( ph -> ( D x. B ) = ( B x. D ) ) |
| 15 |
13 14
|
oveq12d |
|- ( ph -> ( ( C x. B ) + ( D x. B ) ) = ( ( B x. C ) + ( B x. D ) ) ) |
| 16 |
12 15
|
oveq12d |
|- ( ph -> ( ( ( C x. A ) + ( D x. A ) ) - ( ( C x. B ) + ( D x. B ) ) ) = ( ( ( A x. C ) + ( A x. D ) ) - ( ( B x. C ) + ( B x. D ) ) ) ) |
| 17 |
7 9 16
|
3eqtrd |
|- ( ph -> ( ( A - B ) x. ( C + D ) ) = ( ( ( A x. C ) + ( A x. D ) ) - ( ( B x. C ) + ( B x. D ) ) ) ) |