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 e. GrpOp /\ ( A e. X /\ B e. X /\ C e. 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 e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. 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 e. GrpOp /\ C e. X ) -> ( ( ( inv ` G ) ` C ) G C ) = ( GId ` G ) )
7 6 adantlr 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ C e. X ) -> ( ( ( inv ` G ) ` C ) G C ) = ( GId ` G ) )
8 7 oveq1d 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ C e. X ) -> ( ( ( ( inv ` G ) ` C ) G C ) G A ) = ( ( GId ` G ) G A ) )
9 1 5 grpoinvcl 
 |-  ( ( G e. GrpOp /\ C e. X ) -> ( ( inv ` G ) ` C ) e. X )
10 9 adantrl 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ C e. X ) ) -> ( ( inv ` G ) ` C ) e. X )
11 simprr 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ C e. X ) ) -> C e. X )
12 simprl 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ C e. X ) ) -> A e. X )
13 10 11 12 3jca 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ C e. X ) ) -> ( ( ( inv ` G ) ` C ) e. X /\ C e. X /\ A e. X ) )
14 1 grpoass 
 |-  ( ( G e. GrpOp /\ ( ( ( inv ` G ) ` C ) e. X /\ C e. X /\ A e. X ) ) -> ( ( ( ( inv ` G ) ` C ) G C ) G A ) = ( ( ( inv ` G ) ` C ) G ( C G A ) ) )
15 13 14 syldan 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ C e. X ) ) -> ( ( ( ( inv ` G ) ` C ) G C ) G A ) = ( ( ( inv ` G ) ` C ) G ( C G A ) ) )
16 15 anassrs 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ C e. X ) -> ( ( ( ( inv ` G ) ` C ) G C ) G A ) = ( ( ( inv ` G ) ` C ) G ( C G A ) ) )
17 1 4 grpolid 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( ( GId ` G ) G A ) = A )
18 17 adantr 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ C e. X ) -> ( ( GId ` G ) G A ) = A )
19 8 16 18 3eqtr3d 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ C e. X ) -> ( ( ( inv ` G ) ` C ) G ( C G A ) ) = A )
20 19 adantrl 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> ( ( ( inv ` G ) ` C ) G ( C G A ) ) = A )
21 20 adantr 
 |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( C G A ) = ( C G B ) ) -> ( ( ( inv ` G ) ` C ) G ( C G A ) ) = A )
22 6 adantrl 
 |-  ( ( G e. GrpOp /\ ( B e. X /\ C e. X ) ) -> ( ( ( inv ` G ) ` C ) G C ) = ( GId ` G ) )
23 22 oveq1d 
 |-  ( ( G e. GrpOp /\ ( B e. X /\ C e. X ) ) -> ( ( ( ( inv ` G ) ` C ) G C ) G B ) = ( ( GId ` G ) G B ) )
24 9 adantrl 
 |-  ( ( G e. GrpOp /\ ( B e. X /\ C e. X ) ) -> ( ( inv ` G ) ` C ) e. X )
25 simprr 
 |-  ( ( G e. GrpOp /\ ( B e. X /\ C e. X ) ) -> C e. X )
26 simprl 
 |-  ( ( G e. GrpOp /\ ( B e. X /\ C e. X ) ) -> B e. X )
27 24 25 26 3jca 
 |-  ( ( G e. GrpOp /\ ( B e. X /\ C e. X ) ) -> ( ( ( inv ` G ) ` C ) e. X /\ C e. X /\ B e. X ) )
28 1 grpoass 
 |-  ( ( G e. GrpOp /\ ( ( ( inv ` G ) ` C ) e. X /\ C e. X /\ B e. X ) ) -> ( ( ( ( inv ` G ) ` C ) G C ) G B ) = ( ( ( inv ` G ) ` C ) G ( C G B ) ) )
29 27 28 syldan 
 |-  ( ( G e. GrpOp /\ ( B e. X /\ C e. X ) ) -> ( ( ( ( inv ` G ) ` C ) G C ) G B ) = ( ( ( inv ` G ) ` C ) G ( C G B ) ) )
30 1 4 grpolid 
 |-  ( ( G e. GrpOp /\ B e. X ) -> ( ( GId ` G ) G B ) = B )
31 30 adantrr 
 |-  ( ( G e. GrpOp /\ ( B e. X /\ C e. X ) ) -> ( ( GId ` G ) G B ) = B )
32 23 29 31 3eqtr3d 
 |-  ( ( G e. GrpOp /\ ( B e. X /\ C e. X ) ) -> ( ( ( inv ` G ) ` C ) G ( C G B ) ) = B )
33 32 adantlr 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> ( ( ( inv ` G ) ` C ) G ( C G B ) ) = B )
34 33 adantr 
 |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( C G A ) = ( C G B ) ) -> ( ( ( inv ` G ) ` C ) G ( C G B ) ) = B )
35 3 21 34 3eqtr3d 
 |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ ( B e. X /\ C e. X ) ) /\ ( C G A ) = ( C G B ) ) -> A = B )
36 35 exp53 
 |-  ( G e. GrpOp -> ( A e. X -> ( B e. X -> ( C e. X -> ( ( C G A ) = ( C G B ) -> A = B ) ) ) ) )
37 36 3imp2 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( C G A ) = ( C G B ) -> A = B ) )
38 oveq2 
 |-  ( A = B -> ( C G A ) = ( C G B ) )
39 37 38 impbid1 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( C G A ) = ( C G B ) <-> A = B ) )