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