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 fovcdmd ⊢ ⊕ ˙ ∈ 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