Metamath Proof Explorer

Theorem ablodivdiv4

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

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

Proof

Step Hyp Ref Expression
1 abldiv.1 ⊢X=ran⁡G
2 abldiv.3 ⊢D=/g⁡G
3 ablogrpo ⊢G∈AbelOp→G∈GrpOp
4 simpl ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→G∈GrpOp
5 1 2 grpodivcl ⊢G∈GrpOp∧A∈X∧B∈X→ADB∈X
6 5 3adant3r3 ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→ADB∈X
7 simpr3 ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→C∈X
8 eqid ⊢inv⁡G=inv⁡G
9 1 8 2 grpodivval ⊢G∈GrpOp∧ADB∈X∧C∈X→ADBDC=ADBGinv⁡G⁡C
10 4 6 7 9 syl3anc ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→ADBDC=ADBGinv⁡G⁡C
11 3 10 sylan ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→ADBDC=ADBGinv⁡G⁡C
12 simpr1 ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→A∈X
13 simpr2 ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→B∈X
14 simp3 ⊢A∈X∧B∈X∧C∈X→C∈X
15 1 8 grpoinvcl ⊢G∈GrpOp∧C∈X→inv⁡G⁡C∈X
16 3 14 15 syl2an ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→inv⁡G⁡C∈X
17 12 13 16 3jca ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→A∈X∧B∈X∧inv⁡G⁡C∈X
18 1 2 ablodivdiv ⊢G∈AbelOp∧A∈X∧B∈X∧inv⁡G⁡C∈X→ADBDinv⁡G⁡C=ADBGinv⁡G⁡C
19 17 18 syldan ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→ADBDinv⁡G⁡C=ADBGinv⁡G⁡C
20 1 8 2 grpodivinv ⊢G∈GrpOp∧B∈X∧C∈X→BDinv⁡G⁡C=BGC
21 3 20 syl3an1 ⊢G∈AbelOp∧B∈X∧C∈X→BDinv⁡G⁡C=BGC
22 21 3adant3r1 ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→BDinv⁡G⁡C=BGC
23 22 oveq2d ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→ADBDinv⁡G⁡C=ADBGC
24 11 19 23 3eqtr2d ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→ADBDC=ADBGC