Step |
Hyp |
Ref |
Expression |
1 |
|
galcan.1 |
|- X = ( Base ` G ) |
2 |
|
oveq2 |
|- ( ( A .(+) B ) = ( A .(+) C ) -> ( ( ( invg ` G ) ` A ) .(+) ( A .(+) B ) ) = ( ( ( invg ` G ) ` A ) .(+) ( A .(+) C ) ) ) |
3 |
|
simpl |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> .(+) e. ( G GrpAct Y ) ) |
4 |
|
gagrp |
|- ( .(+) e. ( G GrpAct Y ) -> G e. Grp ) |
5 |
3 4
|
syl |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> G e. Grp ) |
6 |
|
simpr1 |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> A e. X ) |
7 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
8 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
9 |
|
eqid |
|- ( invg ` G ) = ( invg ` G ) |
10 |
1 7 8 9
|
grplinv |
|- ( ( G e. Grp /\ A e. X ) -> ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) = ( 0g ` G ) ) |
11 |
5 6 10
|
syl2anc |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) = ( 0g ` G ) ) |
12 |
11
|
oveq1d |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) .(+) B ) = ( ( 0g ` G ) .(+) B ) ) |
13 |
1 9
|
grpinvcl |
|- ( ( G e. Grp /\ A e. X ) -> ( ( invg ` G ) ` A ) e. X ) |
14 |
5 6 13
|
syl2anc |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( invg ` G ) ` A ) e. X ) |
15 |
|
simpr2 |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> B e. Y ) |
16 |
1 7
|
gaass |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( ( ( invg ` G ) ` A ) e. X /\ A e. X /\ B e. Y ) ) -> ( ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) .(+) B ) = ( ( ( invg ` G ) ` A ) .(+) ( A .(+) B ) ) ) |
17 |
3 14 6 15 16
|
syl13anc |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) .(+) B ) = ( ( ( invg ` G ) ` A ) .(+) ( A .(+) B ) ) ) |
18 |
8
|
gagrpid |
|- ( ( .(+) e. ( G GrpAct Y ) /\ B e. Y ) -> ( ( 0g ` G ) .(+) B ) = B ) |
19 |
3 15 18
|
syl2anc |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( 0g ` G ) .(+) B ) = B ) |
20 |
12 17 19
|
3eqtr3d |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( invg ` G ) ` A ) .(+) ( A .(+) B ) ) = B ) |
21 |
11
|
oveq1d |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) .(+) C ) = ( ( 0g ` G ) .(+) C ) ) |
22 |
|
simpr3 |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> C e. Y ) |
23 |
1 7
|
gaass |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( ( ( invg ` G ) ` A ) e. X /\ A e. X /\ C e. Y ) ) -> ( ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) .(+) C ) = ( ( ( invg ` G ) ` A ) .(+) ( A .(+) C ) ) ) |
24 |
3 14 6 22 23
|
syl13anc |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( ( invg ` G ) ` A ) ( +g ` G ) A ) .(+) C ) = ( ( ( invg ` G ) ` A ) .(+) ( A .(+) C ) ) ) |
25 |
8
|
gagrpid |
|- ( ( .(+) e. ( G GrpAct Y ) /\ C e. Y ) -> ( ( 0g ` G ) .(+) C ) = C ) |
26 |
3 22 25
|
syl2anc |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( 0g ` G ) .(+) C ) = C ) |
27 |
21 24 26
|
3eqtr3d |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( invg ` G ) ` A ) .(+) ( A .(+) C ) ) = C ) |
28 |
20 27
|
eqeq12d |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( ( ( invg ` G ) ` A ) .(+) ( A .(+) B ) ) = ( ( ( invg ` G ) ` A ) .(+) ( A .(+) C ) ) <-> B = C ) ) |
29 |
2 28
|
syl5ib |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( A .(+) B ) = ( A .(+) C ) -> B = C ) ) |
30 |
|
oveq2 |
|- ( B = C -> ( A .(+) B ) = ( A .(+) C ) ) |
31 |
29 30
|
impbid1 |
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. Y /\ C e. Y ) ) -> ( ( A .(+) B ) = ( A .(+) C ) <-> B = C ) ) |