# 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 e. GrpOp /\ ( A e. X /\ B e. X /\ C e. 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 e. GrpOp /\ C e. X ) -> ( ( ( ( GId ` G ) G C ) = C /\ ( C G ( GId ` G ) ) = C ) /\ E. y e. 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
` |-  ( E. y e. X ( ( y G C ) = ( GId ` G ) /\ ( C G y ) = ( GId ` G ) ) -> E. y e. X ( C G y ) = ( GId ` G ) )`
` |-  ( ( ( ( ( GId ` G ) G C ) = C /\ ( C G ( GId ` G ) ) = C ) /\ E. y e. X ( ( y G C ) = ( GId ` G ) /\ ( C G y ) = ( GId ` G ) ) ) -> E. y e. X ( C G y ) = ( GId ` G ) )`
7 3 6 syl
` |-  ( ( G e. GrpOp /\ C e. X ) -> E. y e. X ( C G y ) = ( GId ` G ) )`
` |-  ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> E. y e. X ( C G y ) = ( GId ` G ) )`
9 oveq1
` |-  ( ( A G C ) = ( B G C ) -> ( ( A G C ) G y ) = ( ( B G C ) G y ) )`
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( A G C ) = ( B G C ) ) ) -> ( ( A G C ) G y ) = ( ( B G C ) G y ) )`
11 1 grpoass
` |-  ( ( G e. GrpOp /\ ( A e. X /\ C e. X /\ y e. X ) ) -> ( ( A G C ) G y ) = ( A G ( C G y ) ) )`
12 11 3anassrs
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ C e. X ) /\ y e. X ) -> ( ( A G C ) G y ) = ( A G ( C G y ) ) )`
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ y e. X ) -> ( ( A G C ) G y ) = ( A G ( C G y ) ) )`
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( A G C ) = ( B G C ) ) ) -> ( ( A G C ) G y ) = ( A G ( C G y ) ) )`
15 1 grpoass
` |-  ( ( G e. GrpOp /\ ( B e. X /\ C e. X /\ y e. X ) ) -> ( ( B G C ) G y ) = ( B G ( C G y ) ) )`
16 15 3exp2
` |-  ( G e. GrpOp -> ( B e. X -> ( C e. X -> ( y e. X -> ( ( B G C ) G y ) = ( B G ( C G y ) ) ) ) ) )`
17 16 imp42
` |-  ( ( ( G e. GrpOp /\ ( B e. X /\ C e. X ) ) /\ y e. X ) -> ( ( B G C ) G y ) = ( B G ( C G y ) ) )`
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ y e. X ) -> ( ( B G C ) G y ) = ( B G ( C G y ) ) )`
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( A G C ) = ( B G C ) ) ) -> ( ( B G C ) G y ) = ( B G ( C G y ) ) )`
20 10 14 19 3eqtr3d
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( A G C ) = ( B G C ) ) ) -> ( A G ( C G y ) ) = ( B G ( C G y ) ) )`
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. 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 ) ) )`
` |-  ( ( y e. X /\ ( ( C G y ) = ( GId ` G ) /\ ( A G C ) = ( B G C ) ) ) -> ( A G ( C G y ) ) = ( A G ( GId ` G ) ) )`
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. 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 ) ) )`
` |-  ( ( y e. X /\ ( ( C G y ) = ( GId ` G ) /\ ( A G C ) = ( B G C ) ) ) -> ( B G ( C G y ) ) = ( B G ( GId ` G ) ) )`
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. 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 e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. 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 e. GrpOp /\ A e. X ) -> ( A G ( GId ` G ) ) = A )`
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( ( C G y ) = ( GId ` G ) /\ ( A G C ) = ( B G C ) ) ) ) -> ( A G ( GId ` G ) ) = A )`
31 1 2 grporid
` |-  ( ( G e. GrpOp /\ B e. X ) -> ( B G ( GId ` G ) ) = B )`
` |-  ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> ( B G ( GId ` G ) ) = B )`
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( ( C G y ) = ( GId ` G ) /\ ( A G C ) = ( B G C ) ) ) ) -> ( B G ( GId ` G ) ) = B )`
34 28 30 33 3eqtr3d
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( y e. X /\ ( ( C G y ) = ( GId ` G ) /\ ( A G C ) = ( B G C ) ) ) ) -> A = B )`
35 34 exp45
` |-  ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> ( y e. X -> ( ( C G y ) = ( GId ` G ) -> ( ( A G C ) = ( B G C ) -> A = B ) ) ) )`
36 35 rexlimdv
` |-  ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> ( E. y e. X ( C G y ) = ( GId ` G ) -> ( ( A G C ) = ( B G C ) -> A = B ) ) )`
37 8 36 mpd
` |-  ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> ( ( A G C ) = ( B G C ) -> A = B ) )`
38 oveq1
` |-  ( A = B -> ( A G C ) = ( B G C ) )`
39 37 38 impbid1
` |-  ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> ( ( A G C ) = ( B G C ) <-> A = B ) )`
40 39 exp43
` |-  ( G e. GrpOp -> ( A e. X -> ( B e. X -> ( C e. X -> ( ( A G C ) = ( B G C ) <-> A = B ) ) ) ) )`
41 40 3imp2
` |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G C ) = ( B G C ) <-> A = B ) )`