Metamath Proof Explorer

Theorem galcan

Description: The action of a particular group element is left-cancelable. (Contributed by FL, 17-May-2010) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypothesis galcan.1 
|- X = ( Base ` G )
Assertion galcan 
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( A .(+) B ) = ( A .(+) C ) <-> B = C ) )

Proof

Step Hyp Ref Expression
1 galcan.1 
 |-  X = ( Base ` G )
2 oveq2 
 |-  ( ( A .(+) B ) = ( A .(+) C ) -> ( ( ( invg ` G ) ` A ) .(+) ( A .(+) B ) ) = ( ( ( invg ` G ) ` A ) .(+) ( A .(+) C ) ) )
3 simpl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> .(+) e. ( G GrpAct Y ) )
4 gagrp 
 |-  ( .(+) e. ( G GrpAct Y ) -> G e. Grp )
5 3 4 syl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> G e. Grp )
6 simpr1 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> A e. X )
7 eqid 
 |-  ( +g ` G ) = ( +g ` G )
8 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
9 eqid 
 |-  ( invg ` G ) = ( invg ` G )
10 1 7 8 9 grplinv 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) = ( 0g ` G ) )
11 5 6 10 syl2anc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) = ( 0g ` G ) )
12 11 oveq1d 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) .(+) B ) = ( ( 0g ` G ) .(+) B ) )
13 1 9 grpinvcl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( invg ` G ) ` A ) e. X )
14 5 6 13 syl2anc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( invg ` G ) ` A ) e. X )
15 simpr2 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> B e. Y )
16 1 7 gaass 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( ( ( invg ` G ) ` A ) e. X /\ A e. X /\ B e. Y ) ) -> ( ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) .(+) B ) = ( ( ( invg ` G ) ` A ) .(+) ( A .(+) B ) ) )
17 3 14 6 15 16 syl13anc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) .(+) B ) = ( ( ( invg ` G ) ` A ) .(+) ( A .(+) B ) ) )
18 8 gagrpid 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ B e. Y ) -> ( ( 0g ` G ) .(+) B ) = B )
19 3 15 18 syl2anc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( 0g ` G ) .(+) B ) = B )
20 12 17 19 3eqtr3d 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( invg ` G ) ` A ) .(+) ( A .(+) B ) ) = B )
21 11 oveq1d 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) .(+) C ) = ( ( 0g ` G ) .(+) C ) )
22 simpr3 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> C e. Y )
23 1 7 gaass 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( ( ( invg ` G ) ` A ) e. X /\ A e. X /\ C e. Y ) ) -> ( ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) .(+) C ) = ( ( ( invg ` G ) ` A ) .(+) ( A .(+) C ) ) )
24 3 14 6 22 23 syl13anc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) .(+) C ) = ( ( ( invg ` G ) ` A ) .(+) ( A .(+) C ) ) )
25 8 gagrpid 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ C e. Y ) -> ( ( 0g ` G ) .(+) C ) = C )
26 3 22 25 syl2anc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( 0g ` G ) .(+) C ) = C )
27 21 24 26 3eqtr3d 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( invg ` G ) ` A ) .(+) ( A .(+) C ) ) = C )
28 20 27 eqeq12d 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( ( invg ` G ) ` A ) .(+) ( A .(+) B ) ) = ( ( ( invg ` G ) ` A ) .(+) ( A .(+) C ) ) <-> B = C ) )
29 2 28 imbitrid 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( A .(+) B ) = ( A .(+) C ) -> B = C ) )
30 oveq2 
 |-  ( B = C -> ( A .(+) B ) = ( A .(+) C ) )
31 29 30 impbid1 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( A .(+) B ) = ( A .(+) C ) <-> B = C ) )