Theorem ablo32

Description: Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ablcom.1	⊢ 𝑋 = ran 𝐺
Assertion	ablo32	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ablcom.1	⊢ 𝑋 = ran 𝐺
2	1	ablocom	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 𝐺 𝐶 ) = ( 𝐶 𝐺 𝐵 ) )
3	2	3adant3r1	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝐺 𝐶 ) = ( 𝐶 𝐺 𝐵 ) )
4	3	oveq2d	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐺 ( 𝐵 𝐺 𝐶 ) ) = ( 𝐴 𝐺 ( 𝐶 𝐺 𝐵 ) ) )
5		ablogrpo	⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp )
6	1	grpoass	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) = ( 𝐴 𝐺 ( 𝐵 𝐺 𝐶 ) ) )
7	5 6	sylan	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) = ( 𝐴 𝐺 ( 𝐵 𝐺 𝐶 ) ) )
8		3ancomb	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) )
9	1	grpoass	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) = ( 𝐴 𝐺 ( 𝐶 𝐺 𝐵 ) ) )
10	8 9	sylan2b	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) = ( 𝐴 𝐺 ( 𝐶 𝐺 𝐵 ) ) )
11	5 10	sylan	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) = ( 𝐴 𝐺 ( 𝐶 𝐺 𝐵 ) ) )
12	4 7 11	3eqtr4d	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) )