Theorem ablo4

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

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

Proof

Step	Hyp	Ref	Expression
1		ablcom.1	⊢ 𝑋 = ran 𝐺
2		simprll	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → 𝐴 ∈ 𝑋 )
3		simprlr	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → 𝐵 ∈ 𝑋 )
4		simprrl	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → 𝐶 ∈ 𝑋 )
5	2 3 4	3jca	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) )
6	1	ablo32	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) )
7	5 6	syldan	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) )
8	7	oveq1d	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) 𝐺 𝐷 ) = ( ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) 𝐺 𝐷 ) )
9		ablogrpo	⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp )
10	1	grpocl	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
11	10	3expb	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
12	11	adantrr	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
13		simprrl	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → 𝐶 ∈ 𝑋 )
14		simprrr	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → 𝐷 ∈ 𝑋 )
15	12 13 14	3jca	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) )
16	1	grpoass	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) 𝐺 𝐷 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐶 𝐺 𝐷 ) ) )
17	15 16	syldan	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) 𝐺 𝐷 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐶 𝐺 𝐷 ) ) )
18	9 17	sylan	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) 𝐺 𝐷 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐶 𝐺 𝐷 ) ) )
19	1	grpocl	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐶 ) ∈ 𝑋 )
20	19	3expb	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐺 𝐶 ) ∈ 𝑋 )
21	20	adantrlr	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐺 𝐶 ) ∈ 𝑋 )
22	21	adantrrr	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( 𝐴 𝐺 𝐶 ) ∈ 𝑋 )
23		simprlr	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → 𝐵 ∈ 𝑋 )
24	22 23 14	3jca	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( 𝐴 𝐺 𝐶 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) )
25	1	grpoass	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 𝐺 𝐶 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) 𝐺 𝐷 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 ( 𝐵 𝐺 𝐷 ) ) )
26	24 25	syldan	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) 𝐺 𝐷 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 ( 𝐵 𝐺 𝐷 ) ) )
27	9 26	sylan	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) 𝐺 𝐷 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 ( 𝐵 𝐺 𝐷 ) ) )
28	8 18 27	3eqtr3d	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 ( 𝐵 𝐺 𝐷 ) ) )
29	28	3impb	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 ( 𝐵 𝐺 𝐷 ) ) )