Metamath Proof Explorer

Theorem grpolcan

Description: Left cancellation law for groups. (Contributed by NM, 27-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypothesis grplcan.1 ⊢ X = ran ⁡ G
Assertion grpolcan ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C G A = C G B ↔ A = B

Proof

Step Hyp Ref Expression
1 grplcan.1 ⊢ X = ran ⁡ G
2 oveq2 ⊢ C G A = C G B → inv ⁡ G ⁡ C G C G A = inv ⁡ G ⁡ C G C G B
3 2 adantl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ C G A = C G B → inv ⁡ G ⁡ C G C G A = inv ⁡ G ⁡ C G C G B
4 eqid ⊢ GId ⁡ G = GId ⁡ G
5 eqid ⊢ inv ⁡ G = inv ⁡ G
6 1 4 5 grpolinv ⊢ G ∈ GrpOp ∧ C ∈ X → inv ⁡ G ⁡ C G C = GId ⁡ G
7 6 adantlr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C G C = GId ⁡ G
8 7 oveq1d ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C G C G A = GId ⁡ G G A
9 1 5 grpoinvcl ⊢ G ∈ GrpOp ∧ C ∈ X → inv ⁡ G ⁡ C ∈ X
10 9 adantrl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C ∈ X
11 simprr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X → C ∈ X
12 simprl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X → A ∈ X
13 10 11 12 3jca ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C ∈ X ∧ C ∈ X ∧ A ∈ X
14 1 grpoass ⊢ G ∈ GrpOp ∧ inv ⁡ G ⁡ C ∈ X ∧ C ∈ X ∧ A ∈ X → inv ⁡ G ⁡ C G C G A = inv ⁡ G ⁡ C G C G A
15 13 14 syldan ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C G C G A = inv ⁡ G ⁡ C G C G A
16 15 anassrs ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C G C G A = inv ⁡ G ⁡ C G C G A
17 1 4 grpolid ⊢ G ∈ GrpOp ∧ A ∈ X → GId ⁡ G G A = A
18 17 adantr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X → GId ⁡ G G A = A
19 8 16 18 3eqtr3d ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C G C G A = A
20 19 adantrl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C G C G A = A
21 20 adantr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ C G A = C G B → inv ⁡ G ⁡ C G C G A = A
22 6 adantrl ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C G C = GId ⁡ G
23 22 oveq1d ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C G C G B = GId ⁡ G G B
24 9 adantrl ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C ∈ X
25 simprr ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → C ∈ X
26 simprl ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → B ∈ X
27 24 25 26 3jca ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C ∈ X ∧ C ∈ X ∧ B ∈ X
28 1 grpoass ⊢ G ∈ GrpOp ∧ inv ⁡ G ⁡ C ∈ X ∧ C ∈ X ∧ B ∈ X → inv ⁡ G ⁡ C G C G B = inv ⁡ G ⁡ C G C G B
29 27 28 syldan ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C G C G B = inv ⁡ G ⁡ C G C G B
30 1 4 grpolid ⊢ G ∈ GrpOp ∧ B ∈ X → GId ⁡ G G B = B
31 30 adantrr ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → GId ⁡ G G B = B
32 23 29 31 3eqtr3d ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C G C G B = B
33 32 adantlr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → inv ⁡ G ⁡ C G C G B = B
34 33 adantr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ C G A = C G B → inv ⁡ G ⁡ C G C G B = B
35 3 21 34 3eqtr3d ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ C G A = C G B → A = B
36 35 exp53 ⊢ G ∈ GrpOp → A ∈ X → B ∈ X → C ∈ X → C G A = C G B → A = B
37 36 3imp2 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C G A = C G B → A = B
38 oveq2 ⊢ A = B → C G A = C G B
39 37 38 impbid1 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C G A = C G B ↔ A = B