Metamath Proof Explorer

Theorem grpomuldivass

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

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

Proof

Step Hyp Ref Expression
1 grpdivf.1 ⊢X=ran⁡G
2 grpdivf.3 ⊢D=/g⁡G
3 simpr1 ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→A∈X
4 simpr2 ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→B∈X
5 eqid ⊢inv⁡G=inv⁡G
6 1 5 grpoinvcl ⊢G∈GrpOp∧C∈X→inv⁡G⁡C∈X
7 6 3ad2antr3 ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→inv⁡G⁡C∈X
8 3 4 7 3jca ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→A∈X∧B∈X∧inv⁡G⁡C∈X
9 1 grpoass ⊢G∈GrpOp∧A∈X∧B∈X∧inv⁡G⁡C∈X→AGBGinv⁡G⁡C=AGBGinv⁡G⁡C
10 8 9 syldan ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→AGBGinv⁡G⁡C=AGBGinv⁡G⁡C
11 simpl ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→G∈GrpOp
12 1 grpocl ⊢G∈GrpOp∧A∈X∧B∈X→AGB∈X
13 12 3adant3r3 ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→AGB∈X
14 simpr3 ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→C∈X
15 1 5 2 grpodivval ⊢G∈GrpOp∧AGB∈X∧C∈X→AGBDC=AGBGinv⁡G⁡C
16 11 13 14 15 syl3anc ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→AGBDC=AGBGinv⁡G⁡C
17 1 5 2 grpodivval ⊢G∈GrpOp∧B∈X∧C∈X→BDC=BGinv⁡G⁡C
18 17 3adant3r1 ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→BDC=BGinv⁡G⁡C
19 18 oveq2d ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→AGBDC=AGBGinv⁡G⁡C
20 10 16 19 3eqtr4d ⊢G∈GrpOp∧A∈X∧B∈X∧C∈X→AGBDC=AGBDC