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=BaseG
gacan.2 ⊢N=invg⁡G
Assertion gacan ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→A⊕˙B=C↔N⁡A⊕˙C=B

Proof

Step Hyp Ref Expression
1 galcan.1 ⊢X=BaseG
2 gacan.2 ⊢N=invg⁡G
3 gagrp ⊢⊕˙∈GGrpActY→G∈Grp
4 3 adantr ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→G∈Grp
5 simpr1 ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→A∈X
6 eqid ⊢+G=+G
7 eqid ⊢0G=0G
8 1 6 7 2 grprinv ⊢G∈Grp∧A∈X→A+GN⁡A=0G
9 4 5 8 syl2anc ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→A+GN⁡A=0G
10 9 oveq1d ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→A+GN⁡A⊕˙C=0G⊕˙C
11 simpl ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→⊕˙∈GGrpActY
12 1 2 grpinvcl ⊢G∈Grp∧A∈X→N⁡A∈X
13 4 5 12 syl2anc ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→N⁡A∈X
14 simpr3 ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→C∈Y
15 1 6 gaass ⊢⊕˙∈GGrpActY∧A∈X∧N⁡A∈X∧C∈Y→A+GN⁡A⊕˙C=A⊕˙N⁡A⊕˙C
16 11 5 13 14 15 syl13anc ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→A+GN⁡A⊕˙C=A⊕˙N⁡A⊕˙C
17 7 gagrpid ⊢⊕˙∈GGrpActY∧C∈Y→0G⊕˙C=C
18 11 14 17 syl2anc ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→0G⊕˙C=C
19 10 16 18 3eqtr3d ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→A⊕˙N⁡A⊕˙C=C
20 19 eqeq2d ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→A⊕˙B=A⊕˙N⁡A⊕˙C↔A⊕˙B=C
21 simpr2 ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→B∈Y
22 1 gaf ⊢⊕˙∈GGrpActY→⊕˙:X×Y⟶Y
23 22 adantr ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→⊕˙:X×Y⟶Y
24 23 13 14 fovcdmd ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→N⁡A⊕˙C∈Y
25 1 galcan ⊢⊕˙∈GGrpActY∧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 ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→A⊕˙B=A⊕˙N⁡A⊕˙C↔B=N⁡A⊕˙C
27 20 26 bitr3d ⊢⊕˙∈GGrpActY∧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 ⊢⊕˙∈GGrpActY∧A∈X∧B∈Y∧C∈Y→A⊕˙B=C↔N⁡A⊕˙C=B