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

Metamath Proof Explorer

Theorem divmulasscom

Description: An associative/commutative law for division and multiplication. (Contributed by AV, 10-Jul-2021)

Ref Expression
Assertion divmulasscom ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐴 · ( 𝐵 / 𝐷 ) ) · 𝐶 ) = ( 𝐵 · ( ( 𝐴 · 𝐶 ) / 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 divmulass ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐴 · ( 𝐵 / 𝐷 ) ) · 𝐶 ) = ( ( 𝐴 · 𝐵 ) · ( 𝐶 / 𝐷 ) ) )
2 mulcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
3 2 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
4 3 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
5 4 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐴 · 𝐵 ) · ( 𝐶 / 𝐷 ) ) = ( ( 𝐵 · 𝐴 ) · ( 𝐶 / 𝐷 ) ) )
6 simpl2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → 𝐵 ∈ ℂ )
7 simpl1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → 𝐴 ∈ ℂ )
8 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
9 8 anim1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐶 ∈ ℂ ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) )
10 3anass ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ↔ ( 𝐶 ∈ ℂ ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) )
11 9 10 sylibr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) )
12 divcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) → ( 𝐶 / 𝐷 ) ∈ ℂ )
13 11 12 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐶 / 𝐷 ) ∈ ℂ )
14 6 7 13 mulassd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐵 · 𝐴 ) · ( 𝐶 / 𝐷 ) ) = ( 𝐵 · ( 𝐴 · ( 𝐶 / 𝐷 ) ) ) )
15 8 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → 𝐶 ∈ ℂ )
16 simpr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) )
17 divass ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐴 · 𝐶 ) / 𝐷 ) = ( 𝐴 · ( 𝐶 / 𝐷 ) ) )
18 7 15 16 17 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐴 · 𝐶 ) / 𝐷 ) = ( 𝐴 · ( 𝐶 / 𝐷 ) ) )
19 18 eqcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐴 · ( 𝐶 / 𝐷 ) ) = ( ( 𝐴 · 𝐶 ) / 𝐷 ) )
20 19 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐵 · ( 𝐴 · ( 𝐶 / 𝐷 ) ) ) = ( 𝐵 · ( ( 𝐴 · 𝐶 ) / 𝐷 ) ) )
21 14 20 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐵 · 𝐴 ) · ( 𝐶 / 𝐷 ) ) = ( 𝐵 · ( ( 𝐴 · 𝐶 ) / 𝐷 ) ) )
22 1 5 21 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐴 · ( 𝐵 / 𝐷 ) ) · 𝐶 ) = ( 𝐵 · ( ( 𝐴 · 𝐶 ) / 𝐷 ) ) )