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 = inv g G
Assertion gacan ˙ G GrpAct Y A X B Y C Y A ˙ B = C N A ˙ C = B

Proof

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