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