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
|
syl5ib |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 𝐴 ⊕ 𝐵 ) = ( 𝐴 ⊕ 𝐶 ) → 𝐵 = 𝐶 ) ) |
30 |
|
oveq2 |
⊢ ( 𝐵 = 𝐶 → ( 𝐴 ⊕ 𝐵 ) = ( 𝐴 ⊕ 𝐶 ) ) |
31 |
29 30
|
impbid1 |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌 ) ) → ( ( 𝐴 ⊕ 𝐵 ) = ( 𝐴 ⊕ 𝐶 ) ↔ 𝐵 = 𝐶 ) ) |