Theorem mulsubd

Description: Product of two differences. (Contributed by Mario Carneiro, 27-May-2016)

	Ref	Expression
Hypotheses	mulm1d.1	|- ( ph -> A e. CC )
	mulnegd.2	|- ( ph -> B e. CC )
	subdid.3	|- ( ph -> C e. CC )
	muladdd.4	|- ( ph -> D e. CC )
Assertion	mulsubd	|- ( ph -> ( ( A - B ) x. ( C - D ) ) = ( ( ( A x. C ) + ( D x. B ) ) - ( ( A x. D ) + ( C x. B ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulm1d.1	|- ( ph -> A e. CC )
2		mulnegd.2	|- ( ph -> B e. CC )
3		subdid.3	|- ( ph -> C e. CC )
4		muladdd.4	|- ( ph -> D e. CC )
5		mulsub	|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) x. ( C - D ) ) = ( ( ( A x. C ) + ( D x. B ) ) - ( ( A x. D ) + ( C x. B ) ) ) )
6	1 2 3 4 5	syl22anc	|- ( ph -> ( ( A - B ) x. ( C - D ) ) = ( ( ( A x. C ) + ( D x. B ) ) - ( ( A x. D ) + ( C x. B ) ) ) )