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

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 imbitrrdi ⊢ ( 𝐺 ∈ 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 ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐹 ∈ 𝑋 ) ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐷 ( 𝐶 𝐺 𝐹 ) ) = ( ( 𝐴 𝐷 𝐶 ) 𝐺 ( 𝐵 𝐷 𝐹 ) ) )