Metamath Proof Explorer


Theorem mul13d

Description: Commutative/associative law that swaps the first and the third factor in a triple product. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses mul13d.1 ( 𝜑𝐴 ∈ ℂ )
mul13d.2 ( 𝜑𝐵 ∈ ℂ )
mul13d.3 ( 𝜑𝐶 ∈ ℂ )
Assertion mul13d ( 𝜑 → ( 𝐴 · ( 𝐵 · 𝐶 ) ) = ( 𝐶 · ( 𝐵 · 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 mul13d.1 ( 𝜑𝐴 ∈ ℂ )
2 mul13d.2 ( 𝜑𝐵 ∈ ℂ )
3 mul13d.3 ( 𝜑𝐶 ∈ ℂ )
4 1 2 3 mul12d ( 𝜑 → ( 𝐴 · ( 𝐵 · 𝐶 ) ) = ( 𝐵 · ( 𝐴 · 𝐶 ) ) )
5 2 1 3 mulassd ( 𝜑 → ( ( 𝐵 · 𝐴 ) · 𝐶 ) = ( 𝐵 · ( 𝐴 · 𝐶 ) ) )
6 2 1 mulcld ( 𝜑 → ( 𝐵 · 𝐴 ) ∈ ℂ )
7 6 3 mulcomd ( 𝜑 → ( ( 𝐵 · 𝐴 ) · 𝐶 ) = ( 𝐶 · ( 𝐵 · 𝐴 ) ) )
8 4 5 7 3eqtr2d ( 𝜑 → ( 𝐴 · ( 𝐵 · 𝐶 ) ) = ( 𝐶 · ( 𝐵 · 𝐴 ) ) )