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 → A G B D C = A G B D C

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 → A G B G inv ⁡ G ⁡ C = A G B G inv ⁡ G ⁡ C
10 8 9 syldan ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B G inv ⁡ G ⁡ C = A G B G inv ⁡ G ⁡ C
11 simpl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → G ∈ GrpOp
12 1 grpocl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A G B ∈ X
13 12 3adant3r3 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B ∈ X
14 simpr3 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C ∈ X
15 1 5 2 grpodivval ⊢ G ∈ GrpOp ∧ A G B ∈ X ∧ C ∈ X → A G B D C = A G B G inv ⁡ G ⁡ C
16 11 13 14 15 syl3anc ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B D C = A G B G inv ⁡ G ⁡ C
17 1 5 2 grpodivval ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → B D C = B G inv ⁡ G ⁡ C
18 17 3adant3r1 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B D C = B G inv ⁡ G ⁡ C
19 18 oveq2d ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B D C = A G B G inv ⁡ G ⁡ C
20 10 16 19 3eqtr4d ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B D C = A G B D C