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 ) )
6 5 adantl 
 |-  ( ( ( ( ( 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 ) )
8 7 ad2ant2rl 
 |-  ( ( ( 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 ) )
10 9 ad2antll 
 |-  ( ( ( ( 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 ) ) )
13 12 adantlrl 
 |-  ( ( ( ( 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 ) ) )
14 13 adantrr 
 |-  ( ( ( ( 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 ) ) )
18 17 adantllr 
 |-  ( ( ( ( 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 ) ) )
19 18 adantrr 
 |-  ( ( ( ( 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 ) ) )
21 20 adantrrl 
 |-  ( ( ( ( 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 ) ) )
23 22 ad2antrl 
 |-  ( ( y e. 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 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 ) ) )
26 25 ad2antrl 
 |-  ( ( y e. 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 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 )
30 29 ad2antrr 
 |-  ( ( ( ( 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 )
32 31 ad2ant2r 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> ( B G ( GId ` G ) ) = B )
33 32 adantr 
 |-  ( ( ( ( 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 ) )