# Metamath Proof Explorer

## Theorem ablo4pnp

Description: A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010)

Ref Expression
Hypotheses abl4pnp.1 𝑋 = ran 𝐺
abl4pnp.2 𝐷 = ( /𝑔𝐺 )
Assertion ablo4pnp ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐹𝑋 ) ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐷 ( 𝐶 𝐺 𝐹 ) ) = ( ( 𝐴 𝐷 𝐶 ) 𝐺 ( 𝐵 𝐷 𝐹 ) ) )

### Proof

Step Hyp Ref Expression
1 abl4pnp.1 𝑋 = ran 𝐺
2 abl4pnp.2 𝐷 = ( /𝑔𝐺 )
3 df-3an ( ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ↔ ( ( 𝐴𝑋𝐵𝑋 ) ∧ 𝐶𝑋 ) )
4 1 2 ablomuldiv ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐷 𝐶 ) = ( ( 𝐴 𝐷 𝐶 ) 𝐺 𝐵 ) )
5 3 4 sylan2br ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴𝑋𝐵𝑋 ) ∧ 𝐶𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐷 𝐶 ) = ( ( 𝐴 𝐷 𝐶 ) 𝐺 𝐵 ) )
6 5 adantrrr ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐹𝑋 ) ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐷 𝐶 ) = ( ( 𝐴 𝐷 𝐶 ) 𝐺 𝐵 ) )
7 6 oveq1d ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐹𝑋 ) ) ) → ( ( ( 𝐴 𝐺 𝐵 ) 𝐷 𝐶 ) 𝐷 𝐹 ) = ( ( ( 𝐴 𝐷 𝐶 ) 𝐺 𝐵 ) 𝐷 𝐹 ) )
8 ablogrpo ( 𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp )
9 1 grpocl ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
10 9 3expib ( 𝐺 ∈ GrpOp → ( ( 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) )
11 8 10 syl ( 𝐺 ∈ AbelOp → ( ( 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) )
12 11 anim1d ( 𝐺 ∈ AbelOp → ( ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐹𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ ( 𝐶𝑋𝐹𝑋 ) ) ) )
13 3anass ( ( ( 𝐴 𝐺 𝐵 ) ∈ 𝑋𝐶𝑋𝐹𝑋 ) ↔ ( ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ ( 𝐶𝑋𝐹𝑋 ) ) )
14 12 13 syl6ibr ( 𝐺 ∈ AbelOp → ( ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐹𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) ∈ 𝑋𝐶𝑋𝐹𝑋 ) ) )
15 14 imp ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐹𝑋 ) ) ) → ( ( 𝐴 𝐺 𝐵 ) ∈ 𝑋𝐶𝑋𝐹𝑋 ) )
16 1 2 ablodivdiv4 ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 𝐺 𝐵 ) ∈ 𝑋𝐶𝑋𝐹𝑋 ) ) → ( ( ( 𝐴 𝐺 𝐵 ) 𝐷 𝐶 ) 𝐷 𝐹 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐷 ( 𝐶 𝐺 𝐹 ) ) )
17 15 16 syldan ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐹𝑋 ) ) ) → ( ( ( 𝐴 𝐺 𝐵 ) 𝐷 𝐶 ) 𝐷 𝐹 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐷 ( 𝐶 𝐺 𝐹 ) ) )
18 1 2 grpodivcl ( ( 𝐺 ∈ GrpOp ∧ 𝐴𝑋𝐶𝑋 ) → ( 𝐴 𝐷 𝐶 ) ∈ 𝑋 )
19 18 3expib ( 𝐺 ∈ GrpOp → ( ( 𝐴𝑋𝐶𝑋 ) → ( 𝐴 𝐷 𝐶 ) ∈ 𝑋 ) )
20 19 anim1d ( 𝐺 ∈ GrpOp → ( ( ( 𝐴𝑋𝐶𝑋 ) ∧ ( 𝐵𝑋𝐹𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) ∈ 𝑋 ∧ ( 𝐵𝑋𝐹𝑋 ) ) ) )
21 an4 ( ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐹𝑋 ) ) ↔ ( ( 𝐴𝑋𝐶𝑋 ) ∧ ( 𝐵𝑋𝐹𝑋 ) ) )
22 3anass ( ( ( 𝐴 𝐷 𝐶 ) ∈ 𝑋𝐵𝑋𝐹𝑋 ) ↔ ( ( 𝐴 𝐷 𝐶 ) ∈ 𝑋 ∧ ( 𝐵𝑋𝐹𝑋 ) ) )
23 20 21 22 3imtr4g ( 𝐺 ∈ GrpOp → ( ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐹𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) ∈ 𝑋𝐵𝑋𝐹𝑋 ) ) )
24 23 imp ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐹𝑋 ) ) ) → ( ( 𝐴 𝐷 𝐶 ) ∈ 𝑋𝐵𝑋𝐹𝑋 ) )
25 1 2 grpomuldivass ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 𝐷 𝐶 ) ∈ 𝑋𝐵𝑋𝐹𝑋 ) ) → ( ( ( 𝐴 𝐷 𝐶 ) 𝐺 𝐵 ) 𝐷 𝐹 ) = ( ( 𝐴 𝐷 𝐶 ) 𝐺 ( 𝐵 𝐷 𝐹 ) ) )
26 24 25 syldan ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐹𝑋 ) ) ) → ( ( ( 𝐴 𝐷 𝐶 ) 𝐺 𝐵 ) 𝐷 𝐹 ) = ( ( 𝐴 𝐷 𝐶 ) 𝐺 ( 𝐵 𝐷 𝐹 ) ) )
27 8 26 sylan ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐹𝑋 ) ) ) → ( ( ( 𝐴 𝐷 𝐶 ) 𝐺 𝐵 ) 𝐷 𝐹 ) = ( ( 𝐴 𝐷 𝐶 ) 𝐺 ( 𝐵 𝐷 𝐹 ) ) )
28 7 17 27 3eqtr3d ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐹𝑋 ) ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐷 ( 𝐶 𝐺 𝐹 ) ) = ( ( 𝐴 𝐷 𝐶 ) 𝐺 ( 𝐵 𝐷 𝐹 ) ) )