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

Metamath Proof Explorer

Theorem mul4

Description: Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999)

Ref Expression
Assertion mul4 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐵 ) · ( 𝐶 · 𝐷 ) ) = ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 mul32 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) · 𝐵 ) )
2 1 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 · 𝐵 ) · 𝐶 ) · 𝐷 ) = ( ( ( 𝐴 · 𝐶 ) · 𝐵 ) · 𝐷 ) )
3 2 3expa ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 · 𝐵 ) · 𝐶 ) · 𝐷 ) = ( ( ( 𝐴 · 𝐶 ) · 𝐵 ) · 𝐷 ) )
4 3 adantrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐵 ) · 𝐶 ) · 𝐷 ) = ( ( ( 𝐴 · 𝐶 ) · 𝐵 ) · 𝐷 ) )
5 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
6 mulass ⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( ( 𝐴 · 𝐵 ) · 𝐶 ) · 𝐷 ) = ( ( 𝐴 · 𝐵 ) · ( 𝐶 · 𝐷 ) ) )
7 6 3expb ⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐵 ) · 𝐶 ) · 𝐷 ) = ( ( 𝐴 · 𝐵 ) · ( 𝐶 · 𝐷 ) ) )
8 5 7 sylan ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐵 ) · 𝐶 ) · 𝐷 ) = ( ( 𝐴 · 𝐵 ) · ( 𝐶 · 𝐷 ) ) )
9 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
10 mulass ⊢ ( ( ( 𝐴 · 𝐶 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( ( 𝐴 · 𝐶 ) · 𝐵 ) · 𝐷 ) = ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) )
11 10 3expb ⊢ ( ( ( 𝐴 · 𝐶 ) ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐶 ) · 𝐵 ) · 𝐷 ) = ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) )
12 9 11 sylan ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐶 ) · 𝐵 ) · 𝐷 ) = ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) )
13 12 an4s ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 · 𝐶 ) · 𝐵 ) · 𝐷 ) = ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) )
14 4 8 13 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 · 𝐵 ) · ( 𝐶 · 𝐷 ) ) = ( ( 𝐴 · 𝐶 ) · ( 𝐵 · 𝐷 ) ) )