# 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}=\mathrm{ran}{G}$
Assertion grporcan ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{C}={B}{G}{C}↔{A}={B}\right)$

### Proof

Step Hyp Ref Expression
1 grprcan.1 ${⊢}{X}=\mathrm{ran}{G}$
2 eqid ${⊢}\mathrm{GId}\left({G}\right)=\mathrm{GId}\left({G}\right)$
3 1 2 grpoidinv2 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {C}\in {X}\right)\to \left(\left(\mathrm{GId}\left({G}\right){G}{C}={C}\wedge {C}{G}\mathrm{GId}\left({G}\right)={C}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{C}=\mathrm{GId}\left({G}\right)\wedge {C}{G}{y}=\mathrm{GId}\left({G}\right)\right)\right)$
4 simpr ${⊢}\left({y}{G}{C}=\mathrm{GId}\left({G}\right)\wedge {C}{G}{y}=\mathrm{GId}\left({G}\right)\right)\to {C}{G}{y}=\mathrm{GId}\left({G}\right)$
5 4 reximi ${⊢}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{C}=\mathrm{GId}\left({G}\right)\wedge {C}{G}{y}=\mathrm{GId}\left({G}\right)\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{C}{G}{y}=\mathrm{GId}\left({G}\right)$
6 5 adantl ${⊢}\left(\left(\mathrm{GId}\left({G}\right){G}{C}={C}\wedge {C}{G}\mathrm{GId}\left({G}\right)={C}\right)\wedge \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({y}{G}{C}=\mathrm{GId}\left({G}\right)\wedge {C}{G}{y}=\mathrm{GId}\left({G}\right)\right)\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{C}{G}{y}=\mathrm{GId}\left({G}\right)$
7 3 6 syl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {C}\in {X}\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{C}{G}{y}=\mathrm{GId}\left({G}\right)$
8 7 ad2ant2rl ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{C}{G}{y}=\mathrm{GId}\left({G}\right)$
9 oveq1 ${⊢}{A}{G}{C}={B}{G}{C}\to \left({A}{G}{C}\right){G}{y}=\left({B}{G}{C}\right){G}{y}$
10 9 ad2antll ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\wedge \left({y}\in {X}\wedge {A}{G}{C}={B}{G}{C}\right)\right)\to \left({A}{G}{C}\right){G}{y}=\left({B}{G}{C}\right){G}{y}$
11 1 grpoass ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {C}\in {X}\wedge {y}\in {X}\right)\right)\to \left({A}{G}{C}\right){G}{y}={A}{G}\left({C}{G}{y}\right)$
12 11 3anassrs ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge {C}\in {X}\right)\wedge {y}\in {X}\right)\to \left({A}{G}{C}\right){G}{y}={A}{G}\left({C}{G}{y}\right)$
13 12 adantlrl ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\wedge {y}\in {X}\right)\to \left({A}{G}{C}\right){G}{y}={A}{G}\left({C}{G}{y}\right)$
14 13 adantrr ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\wedge \left({y}\in {X}\wedge {A}{G}{C}={B}{G}{C}\right)\right)\to \left({A}{G}{C}\right){G}{y}={A}{G}\left({C}{G}{y}\right)$
15 1 grpoass ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({B}\in {X}\wedge {C}\in {X}\wedge {y}\in {X}\right)\right)\to \left({B}{G}{C}\right){G}{y}={B}{G}\left({C}{G}{y}\right)$
16 15 3exp2 ${⊢}{G}\in \mathrm{GrpOp}\to \left({B}\in {X}\to \left({C}\in {X}\to \left({y}\in {X}\to \left({B}{G}{C}\right){G}{y}={B}{G}\left({C}{G}{y}\right)\right)\right)\right)$
17 16 imp42 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\wedge {y}\in {X}\right)\to \left({B}{G}{C}\right){G}{y}={B}{G}\left({C}{G}{y}\right)$
18 17 adantllr ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\wedge {y}\in {X}\right)\to \left({B}{G}{C}\right){G}{y}={B}{G}\left({C}{G}{y}\right)$
19 18 adantrr ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\wedge \left({y}\in {X}\wedge {A}{G}{C}={B}{G}{C}\right)\right)\to \left({B}{G}{C}\right){G}{y}={B}{G}\left({C}{G}{y}\right)$
20 10 14 19 3eqtr3d ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\wedge \left({y}\in {X}\wedge {A}{G}{C}={B}{G}{C}\right)\right)\to {A}{G}\left({C}{G}{y}\right)={B}{G}\left({C}{G}{y}\right)$
21 20 adantrrl ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\wedge \left({y}\in {X}\wedge \left({C}{G}{y}=\mathrm{GId}\left({G}\right)\wedge {A}{G}{C}={B}{G}{C}\right)\right)\right)\to {A}{G}\left({C}{G}{y}\right)={B}{G}\left({C}{G}{y}\right)$
22 oveq2 ${⊢}{C}{G}{y}=\mathrm{GId}\left({G}\right)\to {A}{G}\left({C}{G}{y}\right)={A}{G}\mathrm{GId}\left({G}\right)$
23 22 ad2antrl ${⊢}\left({y}\in {X}\wedge \left({C}{G}{y}=\mathrm{GId}\left({G}\right)\wedge {A}{G}{C}={B}{G}{C}\right)\right)\to {A}{G}\left({C}{G}{y}\right)={A}{G}\mathrm{GId}\left({G}\right)$
24 23 adantl ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\wedge \left({y}\in {X}\wedge \left({C}{G}{y}=\mathrm{GId}\left({G}\right)\wedge {A}{G}{C}={B}{G}{C}\right)\right)\right)\to {A}{G}\left({C}{G}{y}\right)={A}{G}\mathrm{GId}\left({G}\right)$
25 oveq2 ${⊢}{C}{G}{y}=\mathrm{GId}\left({G}\right)\to {B}{G}\left({C}{G}{y}\right)={B}{G}\mathrm{GId}\left({G}\right)$
26 25 ad2antrl ${⊢}\left({y}\in {X}\wedge \left({C}{G}{y}=\mathrm{GId}\left({G}\right)\wedge {A}{G}{C}={B}{G}{C}\right)\right)\to {B}{G}\left({C}{G}{y}\right)={B}{G}\mathrm{GId}\left({G}\right)$
27 26 adantl ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\wedge \left({y}\in {X}\wedge \left({C}{G}{y}=\mathrm{GId}\left({G}\right)\wedge {A}{G}{C}={B}{G}{C}\right)\right)\right)\to {B}{G}\left({C}{G}{y}\right)={B}{G}\mathrm{GId}\left({G}\right)$
28 21 24 27 3eqtr3d ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\wedge \left({y}\in {X}\wedge \left({C}{G}{y}=\mathrm{GId}\left({G}\right)\wedge {A}{G}{C}={B}{G}{C}\right)\right)\right)\to {A}{G}\mathrm{GId}\left({G}\right)={B}{G}\mathrm{GId}\left({G}\right)$
29 1 2 grporid ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\to {A}{G}\mathrm{GId}\left({G}\right)={A}$
30 29 ad2antrr ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\wedge \left({y}\in {X}\wedge \left({C}{G}{y}=\mathrm{GId}\left({G}\right)\wedge {A}{G}{C}={B}{G}{C}\right)\right)\right)\to {A}{G}\mathrm{GId}\left({G}\right)={A}$
31 1 2 grporid ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {B}\in {X}\right)\to {B}{G}\mathrm{GId}\left({G}\right)={B}$
32 31 ad2ant2r ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\to {B}{G}\mathrm{GId}\left({G}\right)={B}$
33 32 adantr ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\wedge \left({y}\in {X}\wedge \left({C}{G}{y}=\mathrm{GId}\left({G}\right)\wedge {A}{G}{C}={B}{G}{C}\right)\right)\right)\to {B}{G}\mathrm{GId}\left({G}\right)={B}$
34 28 30 33 3eqtr3d ${⊢}\left(\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\wedge \left({y}\in {X}\wedge \left({C}{G}{y}=\mathrm{GId}\left({G}\right)\wedge {A}{G}{C}={B}{G}{C}\right)\right)\right)\to {A}={B}$
35 34 exp45 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({y}\in {X}\to \left({C}{G}{y}=\mathrm{GId}\left({G}\right)\to \left({A}{G}{C}={B}{G}{C}\to {A}={B}\right)\right)\right)$
36 35 rexlimdv ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\to \left(\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{C}{G}{y}=\mathrm{GId}\left({G}\right)\to \left({A}{G}{C}={B}{G}{C}\to {A}={B}\right)\right)$
37 8 36 mpd ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{C}={B}{G}{C}\to {A}={B}\right)$
38 oveq1 ${⊢}{A}={B}\to {A}{G}{C}={B}{G}{C}$
39 37 38 impbid1 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\wedge \left({B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{C}={B}{G}{C}↔{A}={B}\right)$
40 39 exp43 ${⊢}{G}\in \mathrm{GrpOp}\to \left({A}\in {X}\to \left({B}\in {X}\to \left({C}\in {X}\to \left({A}{G}{C}={B}{G}{C}↔{A}={B}\right)\right)\right)\right)$
41 40 3imp2 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{C}={B}{G}{C}↔{A}={B}\right)$