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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion galcan ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 𝐴 ⊕ 𝐵 ) = ( 𝐴 ⊕ 𝐶 ) ↔ 𝐵 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 galcan.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 oveq2 ⊢ ( ( 𝐴 ⊕ 𝐵 ) = ( 𝐴 ⊕ 𝐶 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ ( 𝐴 ⊕ 𝐵 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ ( 𝐴 ⊕ 𝐶 ) ) )
3 simpl ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) )
4 gagrp ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → 𝐺 ∈ Grp )
5 3 4 syl ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → 𝐺 ∈ Grp )
6 simpr1 ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → 𝐴 ∈ 𝑋 )
7 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
8 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
9 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
10 1 7 8 9 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) )
11 5 6 10 syl2anc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) )
12 11 oveq1d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) ⊕ 𝐵 ) = ( ( 0g ‘ 𝐺 ) ⊕ 𝐵 ) )
13 1 9 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 )
14 5 6 13 syl2anc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 )
15 simpr2 ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → 𝐵 ∈ 𝑌 )
16 1 7 gaass ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) ⊕ 𝐵 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ ( 𝐴 ⊕ 𝐵 ) ) )
17 3 14 6 15 16 syl13anc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) ⊕ 𝐵 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ ( 𝐴 ⊕ 𝐵 ) ) )
18 8 gagrpid ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) → ( ( 0g ‘ 𝐺 ) ⊕ 𝐵 ) = 𝐵 )
19 3 15 18 syl2anc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 0g ‘ 𝐺 ) ⊕ 𝐵 ) = 𝐵 )
20 12 17 19 3eqtr3d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ ( 𝐴 ⊕ 𝐵 ) ) = 𝐵 )
21 11 oveq1d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) ⊕ 𝐶 ) = ( ( 0g ‘ 𝐺 ) ⊕ 𝐶 ) )
22 simpr3 ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → 𝐶 ∈ 𝑌 )
23 1 7 gaass ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) ⊕ 𝐶 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ ( 𝐴 ⊕ 𝐶 ) ) )
24 3 14 6 22 23 syl13anc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) ⊕ 𝐶 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ ( 𝐴 ⊕ 𝐶 ) ) )
25 8 gagrpid ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐶 ∈ 𝑌 ) → ( ( 0g ‘ 𝐺 ) ⊕ 𝐶 ) = 𝐶 )
26 3 22 25 syl2anc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 0g ‘ 𝐺 ) ⊕ 𝐶 ) = 𝐶 )
27 21 24 26 3eqtr3d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ ( 𝐴 ⊕ 𝐶 ) ) = 𝐶 )
28 20 27 eqeq12d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ ( 𝐴 ⊕ 𝐵 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ⊕ ( 𝐴 ⊕ 𝐶 ) ) ↔ 𝐵 = 𝐶 ) )
29 2 28 imbitrid ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 𝐴 ⊕ 𝐵 ) = ( 𝐴 ⊕ 𝐶 ) → 𝐵 = 𝐶 ) )
30 oveq2 ⊢ ( 𝐵 = 𝐶 → ( 𝐴 ⊕ 𝐵 ) = ( 𝐴 ⊕ 𝐶 ) )
31 29 30 impbid1 ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 𝐴 ⊕ 𝐵 ) = ( 𝐴 ⊕ 𝐶 ) ↔ 𝐵 = 𝐶 ) )