Metamath Proof Explorer

Theorem grplcan

Description: Left cancellation law for groups. (Contributed by NM, 25-Aug-2011)

Ref Expression
Hypotheses grplcan.b 
|- B = ( Base ` G )
grplcan.p 
|- .+ = ( +g ` G )
Assertion grplcan 
|- ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Z .+ X ) = ( Z .+ Y ) <-> X = Y ) )

Proof

Step Hyp Ref Expression
1 grplcan.b 
 |-  B = ( Base ` G )
2 grplcan.p 
 |-  .+ = ( +g ` G )
3 oveq2 
 |-  ( ( Z .+ X ) = ( Z .+ Y ) -> ( ( ( invg ` G ) ` Z ) .+ ( Z .+ X ) ) = ( ( ( invg ` G ) ` Z ) .+ ( Z .+ Y ) ) )
4 3 adantl 
 |-  ( ( ( ( G e. Grp /\ X e. B ) /\ ( Y e. B /\ Z e. B ) ) /\ ( Z .+ X ) = ( Z .+ Y ) ) -> ( ( ( invg ` G ) ` Z ) .+ ( Z .+ X ) ) = ( ( ( invg ` G ) ` Z ) .+ ( Z .+ Y ) ) )
5 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
6 eqid 
 |-  ( invg ` G ) = ( invg ` G )
7 1 2 5 6 grplinv 
 |-  ( ( G e. Grp /\ Z e. B ) -> ( ( ( invg ` G ) ` Z ) .+ Z ) = ( 0g ` G ) )
8 7 adantlr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ Z e. B ) -> ( ( ( invg ` G ) ` Z ) .+ Z ) = ( 0g ` G ) )
9 8 oveq1d 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ Z e. B ) -> ( ( ( ( invg ` G ) ` Z ) .+ Z ) .+ X ) = ( ( 0g ` G ) .+ X ) )
10 1 6 grpinvcl 
 |-  ( ( G e. Grp /\ Z e. B ) -> ( ( invg ` G ) ` Z ) e. B )
11 10 adantrl 
 |-  ( ( G e. Grp /\ ( X e. B /\ Z e. B ) ) -> ( ( invg ` G ) ` Z ) e. B )
12 simprr 
 |-  ( ( G e. Grp /\ ( X e. B /\ Z e. B ) ) -> Z e. B )
13 simprl 
 |-  ( ( G e. Grp /\ ( X e. B /\ Z e. B ) ) -> X e. B )
14 11 12 13 3jca 
 |-  ( ( G e. Grp /\ ( X e. B /\ Z e. B ) ) -> ( ( ( invg ` G ) ` Z ) e. B /\ Z e. B /\ X e. B ) )
15 1 2 grpass 
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` Z ) e. B /\ Z e. B /\ X e. B ) ) -> ( ( ( ( invg ` G ) ` Z ) .+ Z ) .+ X ) = ( ( ( invg ` G ) ` Z ) .+ ( Z .+ X ) ) )
16 14 15 syldan 
 |-  ( ( G e. Grp /\ ( X e. B /\ Z e. B ) ) -> ( ( ( ( invg ` G ) ` Z ) .+ Z ) .+ X ) = ( ( ( invg ` G ) ` Z ) .+ ( Z .+ X ) ) )
17 16 anassrs 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ Z e. B ) -> ( ( ( ( invg ` G ) ` Z ) .+ Z ) .+ X ) = ( ( ( invg ` G ) ` Z ) .+ ( Z .+ X ) ) )
18 1 2 5 grplid 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( 0g ` G ) .+ X ) = X )
19 18 adantr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ Z e. B ) -> ( ( 0g ` G ) .+ X ) = X )
20 9 17 19 3eqtr3d 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ Z e. B ) -> ( ( ( invg ` G ) ` Z ) .+ ( Z .+ X ) ) = X )
21 20 adantrl 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( Y e. B /\ Z e. B ) ) -> ( ( ( invg ` G ) ` Z ) .+ ( Z .+ X ) ) = X )
22 21 adantr 
 |-  ( ( ( ( G e. Grp /\ X e. B ) /\ ( Y e. B /\ Z e. B ) ) /\ ( Z .+ X ) = ( Z .+ Y ) ) -> ( ( ( invg ` G ) ` Z ) .+ ( Z .+ X ) ) = X )
23 7 adantrl 
 |-  ( ( G e. Grp /\ ( Y e. B /\ Z e. B ) ) -> ( ( ( invg ` G ) ` Z ) .+ Z ) = ( 0g ` G ) )
24 23 oveq1d 
 |-  ( ( G e. Grp /\ ( Y e. B /\ Z e. B ) ) -> ( ( ( ( invg ` G ) ` Z ) .+ Z ) .+ Y ) = ( ( 0g ` G ) .+ Y ) )
25 10 adantrl 
 |-  ( ( G e. Grp /\ ( Y e. B /\ Z e. B ) ) -> ( ( invg ` G ) ` Z ) e. B )
26 simprr 
 |-  ( ( G e. Grp /\ ( Y e. B /\ Z e. B ) ) -> Z e. B )
27 simprl 
 |-  ( ( G e. Grp /\ ( Y e. B /\ Z e. B ) ) -> Y e. B )
28 25 26 27 3jca 
 |-  ( ( G e. Grp /\ ( Y e. B /\ Z e. B ) ) -> ( ( ( invg ` G ) ` Z ) e. B /\ Z e. B /\ Y e. B ) )
29 1 2 grpass 
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` Z ) e. B /\ Z e. B /\ Y e. B ) ) -> ( ( ( ( invg ` G ) ` Z ) .+ Z ) .+ Y ) = ( ( ( invg ` G ) ` Z ) .+ ( Z .+ Y ) ) )
30 28 29 syldan 
 |-  ( ( G e. Grp /\ ( Y e. B /\ Z e. B ) ) -> ( ( ( ( invg ` G ) ` Z ) .+ Z ) .+ Y ) = ( ( ( invg ` G ) ` Z ) .+ ( Z .+ Y ) ) )
31 1 2 5 grplid 
 |-  ( ( G e. Grp /\ Y e. B ) -> ( ( 0g ` G ) .+ Y ) = Y )
32 31 adantrr 
 |-  ( ( G e. Grp /\ ( Y e. B /\ Z e. B ) ) -> ( ( 0g ` G ) .+ Y ) = Y )
33 24 30 32 3eqtr3d 
 |-  ( ( G e. Grp /\ ( Y e. B /\ Z e. B ) ) -> ( ( ( invg ` G ) ` Z ) .+ ( Z .+ Y ) ) = Y )
34 33 adantlr 
 |-  ( ( ( G e. Grp /\ X e. B ) /\ ( Y e. B /\ Z e. B ) ) -> ( ( ( invg ` G ) ` Z ) .+ ( Z .+ Y ) ) = Y )
35 34 adantr 
 |-  ( ( ( ( G e. Grp /\ X e. B ) /\ ( Y e. B /\ Z e. B ) ) /\ ( Z .+ X ) = ( Z .+ Y ) ) -> ( ( ( invg ` G ) ` Z ) .+ ( Z .+ Y ) ) = Y )
36 4 22 35 3eqtr3d 
 |-  ( ( ( ( G e. Grp /\ X e. B ) /\ ( Y e. B /\ Z e. B ) ) /\ ( Z .+ X ) = ( Z .+ Y ) ) -> X = Y )
37 36 exp53 
 |-  ( G e. Grp -> ( X e. B -> ( Y e. B -> ( Z e. B -> ( ( Z .+ X ) = ( Z .+ Y ) -> X = Y ) ) ) ) )
38 37 3imp2 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Z .+ X ) = ( Z .+ Y ) -> X = Y ) )
39 oveq2 
 |-  ( X = Y -> ( Z .+ X ) = ( Z .+ Y ) )
40 38 39 impbid1 
 |-  ( ( G e. Grp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Z .+ X ) = ( Z .+ Y ) <-> X = Y ) )