Metamath Proof Explorer

Theorem gacan

Description: Group inverses cancel in a group action. (Contributed by Jeff Hankins, 11-Aug-2009) (Revised by Mario Carneiro, 13-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 galcan.1 
 |-  X = ( Base ` G )
2 gacan.2 
 |-  N = ( invg ` G )
3 gagrp 
 |-  ( .(+) e. ( G GrpAct Y ) -> G e. Grp )
4 3 adantr 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> G e. Grp )
5 simpr1 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> A e. X )
6 eqid 
 |-  ( +g ` G ) = ( +g ` G )
7 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
8 1 6 7 2 grprinv 
 |-  ( ( G e. Grp /\ A e. X ) -> ( A ( +g ` G ) ( N ` A ) ) = ( 0g ` G ) )
9 4 5 8 syl2anc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( A ( +g ` G ) ( N ` A ) ) = ( 0g ` G ) )
10 9 oveq1d 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( A ( +g ` G ) ( N ` A ) ) .(+) C ) = ( ( 0g ` G ) .(+) C ) )
11 simpl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> .(+) e. ( G GrpAct Y ) )
12 1 2 grpinvcl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( N ` A ) e. X )
13 4 5 12 syl2anc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( N ` A ) e. X )
14 simpr3 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> C e. Y )
15 1 6 gaass 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ ( N ` A ) e. X /\ C e. Y ) ) -> ( ( A ( +g ` G ) ( N ` A ) ) .(+) C ) = ( A .(+) ( ( N ` A ) .(+) C ) ) )
16 11 5 13 14 15 syl13anc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( A ( +g ` G ) ( N ` A ) ) .(+) C ) = ( A .(+) ( ( N ` A ) .(+) C ) ) )
17 7 gagrpid 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ C e. Y ) -> ( ( 0g ` G ) .(+) C ) = C )
18 11 14 17 syl2anc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( 0g ` G ) .(+) C ) = C )
19 10 16 18 3eqtr3d 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( A .(+) ( ( N ` A ) .(+) C ) ) = C )
20 19 eqeq2d 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( A .(+) B ) = ( A .(+) ( ( N ` A ) .(+) C ) ) <-> ( A .(+) B ) = C ) )
21 simpr2 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> B e. Y )
22 1 gaf 
 |-  ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) --> Y )
23 22 adantr 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> .(+) : ( X X. Y ) --> Y )
24 23 13 14 fovrnd 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( N ` A ) .(+) C ) e. Y )
25 1 galcan 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ ( ( N ` A ) .(+) C ) e. Y ) ) -> ( ( A .(+) B ) = ( A .(+) ( ( N ` A ) .(+) C ) ) <-> B = ( ( N ` A ) .(+) C ) ) )
26 11 5 21 24 25 syl13anc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( A .(+) B ) = ( A .(+) ( ( N ` A ) .(+) C ) ) <-> B = ( ( N ` A ) .(+) C ) ) )
27 20 26 bitr3d 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( A .(+) B ) = C <-> B = ( ( N ` A ) .(+) C ) ) )
28 eqcom 
 |-  ( B = ( ( N ` A ) .(+) C ) <-> ( ( N ` A ) .(+) C ) = B )
29 27 28 bitrdi 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( A .(+) B ) = C <-> ( ( N ` A ) .(+) C ) = B ) )