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=BaseG
Assertion galcan ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→A⊕˙B=A⊕˙C↔B=C

Proof

Step Hyp Ref Expression
1 galcan.1 ⊢X=BaseG
2 oveq2 ⊢A⊕˙B=A⊕˙C→invg⁡G⁡A⊕˙A⊕˙B=invg⁡G⁡A⊕˙A⊕˙C
3 simpl ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→⊕˙∈GGrpActY
4 gagrp ⊢⊕˙∈GGrpActY→G∈Grp
5 3 4 syl ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→G∈Grp
6 simpr1 ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→A∈X
7 eqid ⊢+G=+G
8 eqid ⊢0G=0G
9 eqid ⊢invg⁡G=invg⁡G
10 1 7 8 9 grplinv ⊢G∈Grp∧A∈X→invg⁡G⁡A+GA=0G
11 5 6 10 syl2anc ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→invg⁡G⁡A+GA=0G
12 11 oveq1d ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→invg⁡G⁡A+GA⊕˙B=0G⊕˙B
13 1 9 grpinvcl ⊢G∈Grp∧A∈X→invg⁡G⁡A∈X
14 5 6 13 syl2anc ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→invg⁡G⁡A∈X
15 simpr2 ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→B∈Y
16 1 7 gaass ⊢⊕˙∈GGrpActY∧invg⁡G⁡A∈X∧A∈X∧B∈Y→invg⁡G⁡A+GA⊕˙B=invg⁡G⁡A⊕˙A⊕˙B
17 3 14 6 15 16 syl13anc ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→invg⁡G⁡A+GA⊕˙B=invg⁡G⁡A⊕˙A⊕˙B
18 8 gagrpid ⊢⊕˙∈GGrpActY∧B∈Y→0G⊕˙B=B
19 3 15 18 syl2anc ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→0G⊕˙B=B
20 12 17 19 3eqtr3d ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→invg⁡G⁡A⊕˙A⊕˙B=B
21 11 oveq1d ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→invg⁡G⁡A+GA⊕˙C=0G⊕˙C
22 simpr3 ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→C∈Y
23 1 7 gaass ⊢⊕˙∈GGrpActY∧invg⁡G⁡A∈X∧A∈X∧C∈Y→invg⁡G⁡A+GA⊕˙C=invg⁡G⁡A⊕˙A⊕˙C
24 3 14 6 22 23 syl13anc ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→invg⁡G⁡A+GA⊕˙C=invg⁡G⁡A⊕˙A⊕˙C
25 8 gagrpid ⊢⊕˙∈GGrpActY∧C∈Y→0G⊕˙C=C
26 3 22 25 syl2anc ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→0G⊕˙C=C
27 21 24 26 3eqtr3d ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→invg⁡G⁡A⊕˙A⊕˙C=C
28 20 27 eqeq12d ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→invg⁡G⁡A⊕˙A⊕˙B=invg⁡G⁡A⊕˙A⊕˙C↔B=C
29 2 28 imbitrid ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→A⊕˙B=A⊕˙C→B=C
30 oveq2 ⊢B=C→A⊕˙B=A⊕˙C
31 29 30 impbid1 ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→A⊕˙B=A⊕˙C↔B=C