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

Proof

Step Hyp Ref Expression
1 galcan.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 gacan.2 ⊢ 𝑁 = ( invg ‘ 𝐺 )
3 gagrp ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → 𝐺 ∈ Grp )
4 3 adantr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → 𝐺 ∈ Grp )
5 simpr1 ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → 𝐴 ∈ 𝑋 )
6 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
7 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
8 1 6 7 2 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝐴 ) ) = ( 0g ‘ 𝐺 ) )
9 4 5 8 syl2anc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( 𝐴 ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝐴 ) ) = ( 0g ‘ 𝐺 ) )
10 9 oveq1d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 𝐴 ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝐴 ) ) ⊕ 𝐶 ) = ( ( 0g ‘ 𝐺 ) ⊕ 𝐶 ) )
11 simpl ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) )
12 1 2 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 )
13 4 5 12 syl2anc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 )
14 simpr3 ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → 𝐶 ∈ 𝑌 )
15 1 6 gaass ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 𝐴 ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝐴 ) ) ⊕ 𝐶 ) = ( 𝐴 ⊕ ( ( 𝑁 ‘ 𝐴 ) ⊕ 𝐶 ) ) )
16 11 5 13 14 15 syl13anc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 𝐴 ( +g ‘ 𝐺 ) ( 𝑁 ‘ 𝐴 ) ) ⊕ 𝐶 ) = ( 𝐴 ⊕ ( ( 𝑁 ‘ 𝐴 ) ⊕ 𝐶 ) ) )
17 7 gagrpid ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐶 ∈ 𝑌 ) → ( ( 0g ‘ 𝐺 ) ⊕ 𝐶 ) = 𝐶 )
18 11 14 17 syl2anc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 0g ‘ 𝐺 ) ⊕ 𝐶 ) = 𝐶 )
19 10 16 18 3eqtr3d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( 𝐴 ⊕ ( ( 𝑁 ‘ 𝐴 ) ⊕ 𝐶 ) ) = 𝐶 )
20 19 eqeq2d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 𝐴 ⊕ 𝐵 ) = ( 𝐴 ⊕ ( ( 𝑁 ‘ 𝐴 ) ⊕ 𝐶 ) ) ↔ ( 𝐴 ⊕ 𝐵 ) = 𝐶 ) )
21 simpr2 ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → 𝐵 ∈ 𝑌 )
22 1 gaf ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
23 22 adantr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
24 23 13 14 fovrnd ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 𝑁 ‘ 𝐴 ) ⊕ 𝐶 ) ∈ 𝑌 )
25 1 galcan ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ ( ( 𝑁 ‘ 𝐴 ) ⊕ 𝐶 ) ∈ 𝑌 ) ) → ( ( 𝐴 ⊕ 𝐵 ) = ( 𝐴 ⊕ ( ( 𝑁 ‘ 𝐴 ) ⊕ 𝐶 ) ) ↔ 𝐵 = ( ( 𝑁 ‘ 𝐴 ) ⊕ 𝐶 ) ) )
26 11 5 21 24 25 syl13anc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 𝐴 ⊕ 𝐵 ) = ( 𝐴 ⊕ ( ( 𝑁 ‘ 𝐴 ) ⊕ 𝐶 ) ) ↔ 𝐵 = ( ( 𝑁 ‘ 𝐴 ) ⊕ 𝐶 ) ) )
27 20 26 bitr3d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 𝐴 ⊕ 𝐵 ) = 𝐶 ↔ 𝐵 = ( ( 𝑁 ‘ 𝐴 ) ⊕ 𝐶 ) ) )
28 eqcom ⊢ ( 𝐵 = ( ( 𝑁 ‘ 𝐴 ) ⊕ 𝐶 ) ↔ ( ( 𝑁 ‘ 𝐴 ) ⊕ 𝐶 ) = 𝐵 )
29 27 28 bitrdi ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 𝐴 ⊕ 𝐵 ) = 𝐶 ↔ ( ( 𝑁 ‘ 𝐴 ) ⊕ 𝐶 ) = 𝐵 ) )