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 X=ranG
abl4pnp.2 D=/gG
Assertion ablo4pnp GAbelOpAXBXCXFXAGBDCGF=ADCGBDF

Proof

Step Hyp Ref Expression
1 abl4pnp.1 X=ranG
2 abl4pnp.2 D=/gG
3 df-3an AXBXCXAXBXCX
4 1 2 ablomuldiv GAbelOpAXBXCXAGBDC=ADCGB
5 3 4 sylan2br GAbelOpAXBXCXAGBDC=ADCGB
6 5 adantrrr GAbelOpAXBXCXFXAGBDC=ADCGB
7 6 oveq1d GAbelOpAXBXCXFXAGBDCDF=ADCGBDF
8 ablogrpo GAbelOpGGrpOp
9 1 grpocl GGrpOpAXBXAGBX
10 9 3expib GGrpOpAXBXAGBX
11 8 10 syl GAbelOpAXBXAGBX
12 11 anim1d GAbelOpAXBXCXFXAGBXCXFX
13 3anass AGBXCXFXAGBXCXFX
14 12 13 syl6ibr GAbelOpAXBXCXFXAGBXCXFX
15 14 imp GAbelOpAXBXCXFXAGBXCXFX
16 1 2 ablodivdiv4 GAbelOpAGBXCXFXAGBDCDF=AGBDCGF
17 15 16 syldan GAbelOpAXBXCXFXAGBDCDF=AGBDCGF
18 1 2 grpodivcl GGrpOpAXCXADCX
19 18 3expib GGrpOpAXCXADCX
20 19 anim1d GGrpOpAXCXBXFXADCXBXFX
21 an4 AXBXCXFXAXCXBXFX
22 3anass ADCXBXFXADCXBXFX
23 20 21 22 3imtr4g GGrpOpAXBXCXFXADCXBXFX
24 23 imp GGrpOpAXBXCXFXADCXBXFX
25 1 2 grpomuldivass GGrpOpADCXBXFXADCGBDF=ADCGBDF
26 24 25 syldan GGrpOpAXBXCXFXADCGBDF=ADCGBDF
27 8 26 sylan GAbelOpAXBXCXFXADCGBDF=ADCGBDF
28 7 17 27 3eqtr3d GAbelOpAXBXCXFXAGBDCGF=ADCGBDF