Step |
Hyp |
Ref |
Expression |
1 |
|
mulgsubdir.b |
|- B = ( Base ` G ) |
2 |
|
mulgsubdir.t |
|- .x. = ( .g ` G ) |
3 |
|
mulgsubdir.d |
|- .- = ( -g ` G ) |
4 |
|
znegcl |
|- ( N e. ZZ -> -u N e. ZZ ) |
5 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
6 |
1 2 5
|
mulgdir |
|- ( ( G e. Grp /\ ( M e. ZZ /\ -u N e. ZZ /\ X e. B ) ) -> ( ( M + -u N ) .x. X ) = ( ( M .x. X ) ( +g ` G ) ( -u N .x. X ) ) ) |
7 |
4 6
|
syl3anr2 |
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M + -u N ) .x. X ) = ( ( M .x. X ) ( +g ` G ) ( -u N .x. X ) ) ) |
8 |
|
simpr1 |
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> M e. ZZ ) |
9 |
8
|
zcnd |
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> M e. CC ) |
10 |
|
simpr2 |
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> N e. ZZ ) |
11 |
10
|
zcnd |
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> N e. CC ) |
12 |
9 11
|
negsubd |
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( M + -u N ) = ( M - N ) ) |
13 |
12
|
oveq1d |
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M + -u N ) .x. X ) = ( ( M - N ) .x. X ) ) |
14 |
|
eqid |
|- ( invg ` G ) = ( invg ` G ) |
15 |
1 2 14
|
mulgneg |
|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( -u N .x. X ) = ( ( invg ` G ) ` ( N .x. X ) ) ) |
16 |
15
|
3adant3r1 |
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( -u N .x. X ) = ( ( invg ` G ) ` ( N .x. X ) ) ) |
17 |
16
|
oveq2d |
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M .x. X ) ( +g ` G ) ( -u N .x. X ) ) = ( ( M .x. X ) ( +g ` G ) ( ( invg ` G ) ` ( N .x. X ) ) ) ) |
18 |
1 2
|
mulgcl |
|- ( ( G e. Grp /\ M e. ZZ /\ X e. B ) -> ( M .x. X ) e. B ) |
19 |
18
|
3adant3r2 |
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( M .x. X ) e. B ) |
20 |
1 2
|
mulgcl |
|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N .x. X ) e. B ) |
21 |
20
|
3adant3r1 |
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( N .x. X ) e. B ) |
22 |
1 5 14 3
|
grpsubval |
|- ( ( ( M .x. X ) e. B /\ ( N .x. X ) e. B ) -> ( ( M .x. X ) .- ( N .x. X ) ) = ( ( M .x. X ) ( +g ` G ) ( ( invg ` G ) ` ( N .x. X ) ) ) ) |
23 |
19 21 22
|
syl2anc |
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M .x. X ) .- ( N .x. X ) ) = ( ( M .x. X ) ( +g ` G ) ( ( invg ` G ) ` ( N .x. X ) ) ) ) |
24 |
17 23
|
eqtr4d |
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M .x. X ) ( +g ` G ) ( -u N .x. X ) ) = ( ( M .x. X ) .- ( N .x. X ) ) ) |
25 |
7 13 24
|
3eqtr3d |
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M - N ) .x. X ) = ( ( M .x. X ) .- ( N .x. X ) ) ) |