Metamath Proof Explorer

Theorem ablomuldiv

Description: Law for group multiplication and division. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses abldiv.1 ⊢X=ran⁡G
abldiv.3 ⊢D=/g⁡G
Assertion ablomuldiv ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→AGBDC=ADCGB

Proof

Step Hyp Ref Expression
1 abldiv.1 ⊢X=ran⁡G
2 abldiv.3 ⊢D=/g⁡G
3 1 ablocom ⊢G∈AbelOp∧A∈X∧B∈X→AGB=BGA
4 3 3adant3r3 ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→AGB=BGA
5 4 oveq1d ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→AGBDC=BGADC
6 3ancoma ⊢A∈X∧B∈X∧C∈X↔B∈X∧A∈X∧C∈X
7 ablogrpo ⊢G∈AbelOp→G∈GrpOp
8 1 2 grpomuldivass ⊢G∈GrpOp∧B∈X∧A∈X∧C∈X→BGADC=BGADC
9 7 8 sylan ⊢G∈AbelOp∧B∈X∧A∈X∧C∈X→BGADC=BGADC
10 6 9 sylan2b ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→BGADC=BGADC
11 simpr2 ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→B∈X
12 1 2 grpodivcl ⊢G∈GrpOp∧A∈X∧C∈X→ADC∈X
13 7 12 syl3an1 ⊢G∈AbelOp∧A∈X∧C∈X→ADC∈X
14 13 3adant3r2 ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→ADC∈X
15 11 14 jca ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→B∈X∧ADC∈X
16 1 ablocom ⊢G∈AbelOp∧B∈X∧ADC∈X→BGADC=ADCGB
17 16 3expb ⊢G∈AbelOp∧B∈X∧ADC∈X→BGADC=ADCGB
18 15 17 syldan ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→BGADC=ADCGB
19 5 10 18 3eqtrd ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→AGBDC=ADCGB