Metamath Proof Explorer

Theorem addmuldir2d

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

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

Proof

Step Hyp Ref Expression
1 addmuldir2d.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 addmuldir2d.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3 addmuldir2d.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4 addmuldir2d.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
5 addmuldir2d.e ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
6 1 2 3 4 5 3 addmuldir1d ⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐵 · 𝐶 ) ) · ( 𝐷 + ( 𝐸 · 𝐶 ) ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐴 · ( 𝐸 · 𝐶 ) ) ) + ( ( 𝐷 · ( 𝐵 · 𝐶 ) ) + ( ( 𝐵 · 𝐶 ) · ( 𝐸 · 𝐶 ) ) ) ) )
7 1 4 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐷 ) ∈ ℂ )
8 5 3 mulcld ⊢ ( 𝜑 → ( 𝐸 · 𝐶 ) ∈ ℂ )
9 1 8 mulcld ⊢ ( 𝜑 → ( 𝐴 · ( 𝐸 · 𝐶 ) ) ∈ ℂ )
10 7 9 addcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) + ( 𝐴 · ( 𝐸 · 𝐶 ) ) ) ∈ ℂ )
11 2 3 mulcld ⊢ ( 𝜑 → ( 𝐵 · 𝐶 ) ∈ ℂ )
12 4 11 mulcld ⊢ ( 𝜑 → ( 𝐷 · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
13 11 8 mulcld ⊢ ( 𝜑 → ( ( 𝐵 · 𝐶 ) · ( 𝐸 · 𝐶 ) ) ∈ ℂ )
14 10 12 13 addassd ⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐴 · ( 𝐸 · 𝐶 ) ) ) + ( 𝐷 · ( 𝐵 · 𝐶 ) ) ) + ( ( 𝐵 · 𝐶 ) · ( 𝐸 · 𝐶 ) ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐴 · ( 𝐸 · 𝐶 ) ) ) + ( ( 𝐷 · ( 𝐵 · 𝐶 ) ) + ( ( 𝐵 · 𝐶 ) · ( 𝐸 · 𝐶 ) ) ) ) )
15 7 9 12 addassd ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐴 · ( 𝐸 · 𝐶 ) ) ) + ( 𝐷 · ( 𝐵 · 𝐶 ) ) ) = ( ( 𝐴 · 𝐷 ) + ( ( 𝐴 · ( 𝐸 · 𝐶 ) ) + ( 𝐷 · ( 𝐵 · 𝐶 ) ) ) ) )
16 1 5 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐸 ) ∈ ℂ )
17 4 2 mulcld ⊢ ( 𝜑 → ( 𝐷 · 𝐵 ) ∈ ℂ )
18 16 17 3 adddird ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐸 ) + ( 𝐷 · 𝐵 ) ) · 𝐶 ) = ( ( ( 𝐴 · 𝐸 ) · 𝐶 ) + ( ( 𝐷 · 𝐵 ) · 𝐶 ) ) )
19 1 5 3 mulassd ⊢ ( 𝜑 → ( ( 𝐴 · 𝐸 ) · 𝐶 ) = ( 𝐴 · ( 𝐸 · 𝐶 ) ) )
20 4 2 3 mulassd ⊢ ( 𝜑 → ( ( 𝐷 · 𝐵 ) · 𝐶 ) = ( 𝐷 · ( 𝐵 · 𝐶 ) ) )
21 19 20 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐸 ) · 𝐶 ) + ( ( 𝐷 · 𝐵 ) · 𝐶 ) ) = ( ( 𝐴 · ( 𝐸 · 𝐶 ) ) + ( 𝐷 · ( 𝐵 · 𝐶 ) ) ) )
22 18 21 eqtr2d ⊢ ( 𝜑 → ( ( 𝐴 · ( 𝐸 · 𝐶 ) ) + ( 𝐷 · ( 𝐵 · 𝐶 ) ) ) = ( ( ( 𝐴 · 𝐸 ) + ( 𝐷 · 𝐵 ) ) · 𝐶 ) )
23 22 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) + ( ( 𝐴 · ( 𝐸 · 𝐶 ) ) + ( 𝐷 · ( 𝐵 · 𝐶 ) ) ) ) = ( ( 𝐴 · 𝐷 ) + ( ( ( 𝐴 · 𝐸 ) + ( 𝐷 · 𝐵 ) ) · 𝐶 ) ) )
24 15 23 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐴 · ( 𝐸 · 𝐶 ) ) ) + ( 𝐷 · ( 𝐵 · 𝐶 ) ) ) = ( ( 𝐴 · 𝐷 ) + ( ( ( 𝐴 · 𝐸 ) + ( 𝐷 · 𝐵 ) ) · 𝐶 ) ) )
25 2 3 5 3 mul4d ⊢ ( 𝜑 → ( ( 𝐵 · 𝐶 ) · ( 𝐸 · 𝐶 ) ) = ( ( 𝐵 · 𝐸 ) · ( 𝐶 · 𝐶 ) ) )
26 sqval ⊢ ( 𝐶 ∈ ℂ → ( 𝐶 ↑ 2 ) = ( 𝐶 · 𝐶 ) )
27 26 eqcomd ⊢ ( 𝐶 ∈ ℂ → ( 𝐶 · 𝐶 ) = ( 𝐶 ↑ 2 ) )
28 3 27 syl ⊢ ( 𝜑 → ( 𝐶 · 𝐶 ) = ( 𝐶 ↑ 2 ) )
29 28 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 · 𝐸 ) · ( 𝐶 · 𝐶 ) ) = ( ( 𝐵 · 𝐸 ) · ( 𝐶 ↑ 2 ) ) )
30 25 29 eqtrd ⊢ ( 𝜑 → ( ( 𝐵 · 𝐶 ) · ( 𝐸 · 𝐶 ) ) = ( ( 𝐵 · 𝐸 ) · ( 𝐶 ↑ 2 ) ) )
31 24 30 oveq12d ⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐴 · ( 𝐸 · 𝐶 ) ) ) + ( 𝐷 · ( 𝐵 · 𝐶 ) ) ) + ( ( 𝐵 · 𝐶 ) · ( 𝐸 · 𝐶 ) ) ) = ( ( ( 𝐴 · 𝐷 ) + ( ( ( 𝐴 · 𝐸 ) + ( 𝐷 · 𝐵 ) ) · 𝐶 ) ) + ( ( 𝐵 · 𝐸 ) · ( 𝐶 ↑ 2 ) ) ) )
32 6 14 31 3eqtr2d ⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐵 · 𝐶 ) ) · ( 𝐷 + ( 𝐸 · 𝐶 ) ) ) = ( ( ( 𝐴 · 𝐷 ) + ( ( ( 𝐴 · 𝐸 ) + ( 𝐷 · 𝐵 ) ) · 𝐶 ) ) + ( ( 𝐵 · 𝐸 ) · ( 𝐶 ↑ 2 ) ) ) )