This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → ( 𝐸 − ( ( 𝐴 + 𝐵 ) · ( 𝐶 − 𝐷 ) ) ) = ( ( ( 𝐸 − ( 𝐴 · 𝐶 ) ) − ( 𝐵 · 𝐶 ) ) + ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		addmulsub	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) · ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) − ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) )
2	1	3adant3	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) · ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) − ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) )
3	2	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → ( 𝐸 − ( ( 𝐴 + 𝐵 ) · ( 𝐶 − 𝐷 ) ) ) = ( 𝐸 − ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) − ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) ) )
4		simp3	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → 𝐸 ∈ ℂ )
5		simp1l	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → 𝐴 ∈ ℂ )
6		simp2l	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → 𝐶 ∈ ℂ )
7	5 6	mulcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
8		simp1r	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → 𝐵 ∈ ℂ )
9	8 6	mulcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
10	7 9	addcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) ∈ ℂ )
11		simp2r	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → 𝐷 ∈ ℂ )
12	5 11	mulcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → ( 𝐴 · 𝐷 ) ∈ ℂ )
13	8 11	mulcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → ( 𝐵 · 𝐷 ) ∈ ℂ )
14	12 13	addcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ∈ ℂ )
15	4 10 14	subsubd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → ( 𝐸 − ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) − ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) ) = ( ( 𝐸 − ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) ) + ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) )
16	4 7 9	subsub4d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → ( ( 𝐸 − ( 𝐴 · 𝐶 ) ) − ( 𝐵 · 𝐶 ) ) = ( 𝐸 − ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) ) )
17	16	eqcomd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → ( 𝐸 − ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) ) = ( ( 𝐸 − ( 𝐴 · 𝐶 ) ) − ( 𝐵 · 𝐶 ) ) )
18	17	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → ( ( 𝐸 − ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐶 ) ) ) + ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) = ( ( ( 𝐸 − ( 𝐴 · 𝐶 ) ) − ( 𝐵 · 𝐶 ) ) + ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) )
19	3 15 18	3eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐸 ∈ ℂ ) → ( 𝐸 − ( ( 𝐴 + 𝐵 ) · ( 𝐶 − 𝐷 ) ) ) = ( ( ( 𝐸 − ( 𝐴 · 𝐶 ) ) − ( 𝐵 · 𝐶 ) ) + ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐷 ) ) ) )