Theorem submuladdd

Description: The product of a difference and a sum. Cf. addmulsub . (Contributed by Thierry Arnoux, 6-Jul-2025)

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

Proof

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