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 ) ) → ( ( 𝐴 · ( 𝐵 / 𝐷 ) ) · 𝐶 ) = ( 𝐵 · ( ( 𝐴 · 𝐶 ) / 𝐷 ) ) )