Theorem addmuldir1d

Description: Distributive law with summands being products. (Contributed by AV, 25-Oct-2026)

	Ref	Expression
Hypotheses	addmuldir1d.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	addmuldir1d.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	addmuldir1d.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	addmuldir1d.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
	addmuldir1d.e	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
	addmuldir1d.f	⊢ ( 𝜑 → 𝐹 ∈ ℂ )
Assertion	addmuldir1d	⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐵 · 𝐶 ) ) · ( 𝐷 + ( 𝐸 · 𝐹 ) ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐴 · ( 𝐸 · 𝐹 ) ) ) + ( ( 𝐷 · ( 𝐵 · 𝐶 ) ) + ( ( 𝐵 · 𝐶 ) · ( 𝐸 · 𝐹 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		addmuldir1d.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		addmuldir1d.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		addmuldir1d.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		addmuldir1d.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
5		addmuldir1d.e	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
6		addmuldir1d.f	⊢ ( 𝜑 → 𝐹 ∈ ℂ )
7	2 3	mulcld	⊢ ( 𝜑 → ( 𝐵 · 𝐶 ) ∈ ℂ )
8	5 6	mulcld	⊢ ( 𝜑 → ( 𝐸 · 𝐹 ) ∈ ℂ )
9	1 7 4 8	muladdd	⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐵 · 𝐶 ) ) · ( 𝐷 + ( 𝐸 · 𝐹 ) ) ) = ( ( ( 𝐴 · 𝐷 ) + ( ( 𝐸 · 𝐹 ) · ( 𝐵 · 𝐶 ) ) ) + ( ( 𝐴 · ( 𝐸 · 𝐹 ) ) + ( 𝐷 · ( 𝐵 · 𝐶 ) ) ) ) )
10	1 4	mulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐷 ) ∈ ℂ )
11	8 7	mulcld	⊢ ( 𝜑 → ( ( 𝐸 · 𝐹 ) · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
12	1 8	mulcld	⊢ ( 𝜑 → ( 𝐴 · ( 𝐸 · 𝐹 ) ) ∈ ℂ )
13	4 7	mulcld	⊢ ( 𝜑 → ( 𝐷 · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
14	10 11 12 13	add42d	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( ( 𝐸 · 𝐹 ) · ( 𝐵 · 𝐶 ) ) ) + ( ( 𝐴 · ( 𝐸 · 𝐹 ) ) + ( 𝐷 · ( 𝐵 · 𝐶 ) ) ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐴 · ( 𝐸 · 𝐹 ) ) ) + ( ( 𝐷 · ( 𝐵 · 𝐶 ) ) + ( ( 𝐸 · 𝐹 ) · ( 𝐵 · 𝐶 ) ) ) ) )
15	8 7	mulcomd	⊢ ( 𝜑 → ( ( 𝐸 · 𝐹 ) · ( 𝐵 · 𝐶 ) ) = ( ( 𝐵 · 𝐶 ) · ( 𝐸 · 𝐹 ) ) )
16	15	oveq2d	⊢ ( 𝜑 → ( ( 𝐷 · ( 𝐵 · 𝐶 ) ) + ( ( 𝐸 · 𝐹 ) · ( 𝐵 · 𝐶 ) ) ) = ( ( 𝐷 · ( 𝐵 · 𝐶 ) ) + ( ( 𝐵 · 𝐶 ) · ( 𝐸 · 𝐹 ) ) ) )
17	16	oveq2d	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐴 · ( 𝐸 · 𝐹 ) ) ) + ( ( 𝐷 · ( 𝐵 · 𝐶 ) ) + ( ( 𝐸 · 𝐹 ) · ( 𝐵 · 𝐶 ) ) ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐴 · ( 𝐸 · 𝐹 ) ) ) + ( ( 𝐷 · ( 𝐵 · 𝐶 ) ) + ( ( 𝐵 · 𝐶 ) · ( 𝐸 · 𝐹 ) ) ) ) )
18	9 14 17	3eqtrd	⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐵 · 𝐶 ) ) · ( 𝐷 + ( 𝐸 · 𝐹 ) ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐴 · ( 𝐸 · 𝐹 ) ) ) + ( ( 𝐷 · ( 𝐵 · 𝐶 ) ) + ( ( 𝐵 · 𝐶 ) · ( 𝐸 · 𝐹 ) ) ) ) )