Metamath Proof Explorer

Theorem subaddmulsub

Description: The difference with a product of a sum and a difference. (Contributed by AV, 5-Mar-2023)

		Ref	Expression
	Assertion	subaddmulsub	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( E - ( ( A + B ) x. ( C - D ) ) ) = ( ( ( E - ( A x. C ) ) - ( B x. C ) ) + ( ( A x. D ) + ( B x. D ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		addmulsub	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) x. ( C - D ) ) = ( ( ( A x. C ) + ( B x. C ) ) - ( ( A x. D ) + ( B x. D ) ) ) )
2	1	3adant3	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( ( A + B ) x. ( C - D ) ) = ( ( ( A x. C ) + ( B x. C ) ) - ( ( A x. D ) + ( B x. D ) ) ) )
3	2	oveq2d	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( E - ( ( A + B ) x. ( C - D ) ) ) = ( E - ( ( ( A x. C ) + ( B x. C ) ) - ( ( A x. D ) + ( B x. D ) ) ) ) )
4		simp3	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> E e. CC )
5		simp1l	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> A e. CC )
6		simp2l	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> C e. CC )
7	5 6	mulcld	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( A x. C ) e. CC )
8		simp1r	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> B e. CC )
9	8 6	mulcld	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( B x. C ) e. CC )
10	7 9	addcld	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( ( A x. C ) + ( B x. C ) ) e. CC )
11		simp2r	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> D e. CC )
12	5 11	mulcld	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( A x. D ) e. CC )
13	8 11	mulcld	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( B x. D ) e. CC )
14	12 13	addcld	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( ( A x. D ) + ( B x. D ) ) e. CC )
15	4 10 14	subsubd	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( E - ( ( ( A x. C ) + ( B x. C ) ) - ( ( A x. D ) + ( B x. D ) ) ) ) = ( ( E - ( ( A x. C ) + ( B x. C ) ) ) + ( ( A x. D ) + ( B x. D ) ) ) )
16	4 7 9	subsub4d	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( ( E - ( A x. C ) ) - ( B x. C ) ) = ( E - ( ( A x. C ) + ( B x. C ) ) ) )
17	16	eqcomd	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( E - ( ( A x. C ) + ( B x. C ) ) ) = ( ( E - ( A x. C ) ) - ( B x. C ) ) )
18	17	oveq1d	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( ( E - ( ( A x. C ) + ( B x. C ) ) ) + ( ( A x. D ) + ( B x. D ) ) ) = ( ( ( E - ( A x. C ) ) - ( B x. C ) ) + ( ( A x. D ) + ( B x. D ) ) ) )
19	3 15 18	3eqtrd	\|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ E e. CC ) -> ( E - ( ( A + B ) x. ( C - D ) ) ) = ( ( ( E - ( A x. C ) ) - ( B x. C ) ) + ( ( A x. D ) + ( B x. D ) ) ) )