Metamath Proof Explorer

Theorem grpodivdiv

Description: Double group division. (Contributed by NM, 24-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses grpdivf.1 ⊢X=ran⁡G
grpdivf.3 ⊢D=/g⁡G
Assertion grpodivdiv ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→ADBDC=AGCDB

Proof

Step Hyp Ref Expression
1 grpdivf.1 ⊢X=ran⁡G
2 grpdivf.3 ⊢D=/g⁡G
3 simpl ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→G∈GrpOp
4 simpr1 ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→A∈X
5 1 2 grpodivcl ⊢G∈GrpOp∧B∈X∧C∈X→BDC∈X
6 5 3adant3r1 ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→BDC∈X
7 eqid ⊢inv⁡G=inv⁡G
8 1 7 2 grpodivval ⊢G∈GrpOp∧A∈X∧BDC∈X→ADBDC=AGinv⁡G⁡BDC
9 3 4 6 8 syl3anc ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→ADBDC=AGinv⁡G⁡BDC
10 1 7 2 grpoinvdiv ⊢G∈GrpOp∧B∈X∧C∈X→inv⁡G⁡BDC=CDB
11 10 3adant3r1 ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→inv⁡G⁡BDC=CDB
12 11 oveq2d ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→AGinv⁡G⁡BDC=AGCDB
13 9 12 eqtrd ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→ADBDC=AGCDB