Metamath Proof Explorer

Theorem grporcan

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

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

Proof

Step Hyp Ref Expression
1 grprcan.1 ⊢ X = ran ⁡ G
2 eqid ⊢ GId ⁡ G = GId ⁡ G
3 1 2 grpoidinv2 ⊢ G ∈ GrpOp ∧ C ∈ X → GId ⁡ G G C = C ∧ C G GId ⁡ G = C ∧ ∃ y ∈ X y G C = GId ⁡ G ∧ C G y = GId ⁡ G
4 simpr ⊢ y G C = GId ⁡ G ∧ C G y = GId ⁡ G → C G y = GId ⁡ G
5 4 reximi ⊢ ∃ y ∈ X y G C = GId ⁡ G ∧ C G y = GId ⁡ G → ∃ y ∈ X C G y = GId ⁡ G
6 5 adantl ⊢ GId ⁡ G G C = C ∧ C G GId ⁡ G = C ∧ ∃ y ∈ X y G C = GId ⁡ G ∧ C G y = GId ⁡ G → ∃ y ∈ X C G y = GId ⁡ G
7 3 6 syl ⊢ G ∈ GrpOp ∧ C ∈ X → ∃ y ∈ X C G y = GId ⁡ G
8 7 ad2ant2rl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → ∃ y ∈ X C G y = GId ⁡ G
9 oveq1 ⊢ A G C = B G C → A G C G y = B G C G y
10 9 ad2antll ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ y ∈ X ∧ A G C = B G C → A G C G y = B G C G y
11 1 grpoass ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X ∧ y ∈ X → A G C G y = A G C G y
12 11 3anassrs ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X ∧ y ∈ X → A G C G y = A G C G y
13 12 adantlrl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ y ∈ X → A G C G y = A G C G y
14 13 adantrr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ y ∈ X ∧ A G C = B G C → A G C G y = A G C G y
15 1 grpoass ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X ∧ y ∈ X → B G C G y = B G C G y
16 15 3exp2 ⊢ G ∈ GrpOp → B ∈ X → C ∈ X → y ∈ X → B G C G y = B G C G y
17 16 imp42 ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X ∧ y ∈ X → B G C G y = B G C G y
18 17 adantllr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ y ∈ X → B G C G y = B G C G y
19 18 adantrr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ y ∈ X ∧ A G C = B G C → B G C G y = B G C G y
20 10 14 19 3eqtr3d ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ y ∈ X ∧ A G C = B G C → A G C G y = B G C G y
21 20 adantrrl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ y ∈ X ∧ C G y = GId ⁡ G ∧ A G C = B G C → A G C G y = B G C G y
22 oveq2 ⊢ C G y = GId ⁡ G → A G C G y = A G GId ⁡ G
23 22 ad2antrl ⊢ y ∈ X ∧ C G y = GId ⁡ G ∧ A G C = B G C → A G C G y = A G GId ⁡ G
24 23 adantl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ y ∈ X ∧ C G y = GId ⁡ G ∧ A G C = B G C → A G C G y = A G GId ⁡ G
25 oveq2 ⊢ C G y = GId ⁡ G → B G C G y = B G GId ⁡ G
26 25 ad2antrl ⊢ y ∈ X ∧ C G y = GId ⁡ G ∧ A G C = B G C → B G C G y = B G GId ⁡ G
27 26 adantl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ y ∈ X ∧ C G y = GId ⁡ G ∧ A G C = B G C → B G C G y = B G GId ⁡ G
28 21 24 27 3eqtr3d ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ y ∈ X ∧ C G y = GId ⁡ G ∧ A G C = B G C → A G GId ⁡ G = B G GId ⁡ G
29 1 2 grporid ⊢ G ∈ GrpOp ∧ A ∈ X → A G GId ⁡ G = A
30 29 ad2antrr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ y ∈ X ∧ C G y = GId ⁡ G ∧ A G C = B G C → A G GId ⁡ G = A
31 1 2 grporid ⊢ G ∈ GrpOp ∧ B ∈ X → B G GId ⁡ G = B
32 31 ad2ant2r ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B G GId ⁡ G = B
33 32 adantr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ y ∈ X ∧ C G y = GId ⁡ G ∧ A G C = B G C → B G GId ⁡ G = B
34 28 30 33 3eqtr3d ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ y ∈ X ∧ C G y = GId ⁡ G ∧ A G C = B G C → A = B
35 34 exp45 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → y ∈ X → C G y = GId ⁡ G → A G C = B G C → A = B
36 35 rexlimdv ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → ∃ y ∈ X C G y = GId ⁡ G → A G C = B G C → A = B
37 8 36 mpd ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G C = B G C → A = B
38 oveq1 ⊢ A = B → A G C = B G C
39 37 38 impbid1 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G C = B G C ↔ A = B
40 39 exp43 ⊢ G ∈ GrpOp → A ∈ X → B ∈ X → C ∈ X → A G C = B G C ↔ A = B
41 40 3imp2 ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G C = B G C ↔ A = B