Metamath Proof Explorer

Theorem ablo4

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

Ref Expression
Hypothesis ablcom.1 ⊢X=ran⁡G
Assertion ablo4 ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X∧D∈X→AGBGCGD=AGCGBGD

Proof

Step Hyp Ref Expression
1 ablcom.1 ⊢X=ran⁡G
2 simprll ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X∧D∈X→A∈X
3 simprlr ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X∧D∈X→B∈X
4 simprrl ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X∧D∈X→C∈X
5 2 3 4 3jca ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X∧D∈X→A∈X∧B∈X∧C∈X
6 1 ablo32 ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→AGBGC=AGCGB
7 5 6 syldan ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X∧D∈X→AGBGC=AGCGB
8 7 oveq1d ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X∧D∈X→AGBGCGD=AGCGBGD
9 ablogrpo ⊢G∈AbelOp→G∈GrpOp
10 1 grpocl ⊢G∈GrpOp∧A∈X∧B∈X→AGB∈X
11 10 3expb ⊢G∈GrpOp∧A∈X∧B∈X→AGB∈X
12 11 adantrr ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X∧D∈X→AGB∈X
13 simprrl ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X∧D∈X→C∈X
14 simprrr ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X∧D∈X→D∈X
15 12 13 14 3jca ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X∧D∈X→AGB∈X∧C∈X∧D∈X
16 1 grpoass ⊢G∈GrpOp∧AGB∈X∧C∈X∧D∈X→AGBGCGD=AGBGCGD
17 15 16 syldan ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X∧D∈X→AGBGCGD=AGBGCGD
18 9 17 sylan ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X∧D∈X→AGBGCGD=AGBGCGD
19 1 grpocl ⊢G∈GrpOp∧A∈X∧C∈X→AGC∈X
20 19 3expb ⊢G∈GrpOp∧A∈X∧C∈X→AGC∈X
21 20 adantrlr ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→AGC∈X
22 21 adantrrr ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X∧D∈X→AGC∈X
23 simprlr ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X∧D∈X→B∈X
24 22 23 14 3jca ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X∧D∈X→AGC∈X∧B∈X∧D∈X
25 1 grpoass ⊢G∈GrpOp∧AGC∈X∧B∈X∧D∈X→AGCGBGD=AGCGBGD
26 24 25 syldan ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X∧D∈X→AGCGBGD=AGCGBGD
27 9 26 sylan ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X∧D∈X→AGCGBGD=AGCGBGD
28 8 18 27 3eqtr3d ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X∧D∈X→AGBGCGD=AGCGBGD
29 28 3impb ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X∧D∈X→AGBGCGD=AGCGBGD