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 ˙ G GrpAct Y A X B Y C Y A ˙ B = A ˙ C B = C

Proof

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