Step |
Hyp |
Ref |
Expression |
1 |
|
mulgnncl.b |
|- B = ( Base ` G ) |
2 |
|
mulgnncl.t |
|- .x. = ( .g ` G ) |
3 |
|
mulgneg.i |
|- I = ( invg ` G ) |
4 |
|
elnn0 |
|- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) ) |
5 |
|
simpr |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N e. NN ) -> N e. NN ) |
6 |
|
simpl3 |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N e. NN ) -> X e. B ) |
7 |
1 2 3
|
mulgnegnn |
|- ( ( N e. NN /\ X e. B ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) ) |
8 |
5 6 7
|
syl2anc |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N e. NN ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) ) |
9 |
|
simpl1 |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> G e. Grp ) |
10 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
11 |
10 3
|
grpinvid |
|- ( G e. Grp -> ( I ` ( 0g ` G ) ) = ( 0g ` G ) ) |
12 |
9 11
|
syl |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( I ` ( 0g ` G ) ) = ( 0g ` G ) ) |
13 |
|
simpr |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> N = 0 ) |
14 |
13
|
oveq1d |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( N .x. X ) = ( 0 .x. X ) ) |
15 |
|
simpl3 |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> X e. B ) |
16 |
1 10 2
|
mulg0 |
|- ( X e. B -> ( 0 .x. X ) = ( 0g ` G ) ) |
17 |
15 16
|
syl |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( 0 .x. X ) = ( 0g ` G ) ) |
18 |
14 17
|
eqtrd |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( N .x. X ) = ( 0g ` G ) ) |
19 |
18
|
fveq2d |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( I ` ( N .x. X ) ) = ( I ` ( 0g ` G ) ) ) |
20 |
13
|
negeqd |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> -u N = -u 0 ) |
21 |
|
neg0 |
|- -u 0 = 0 |
22 |
20 21
|
eqtrdi |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> -u N = 0 ) |
23 |
22
|
oveq1d |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( -u N .x. X ) = ( 0 .x. X ) ) |
24 |
23 17
|
eqtrd |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( -u N .x. X ) = ( 0g ` G ) ) |
25 |
12 19 24
|
3eqtr4rd |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) ) |
26 |
8 25
|
jaodan |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. NN \/ N = 0 ) ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) ) |
27 |
4 26
|
sylan2b |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N e. NN0 ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) ) |
28 |
|
simpl1 |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> G e. Grp ) |
29 |
|
simprr |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. NN ) |
30 |
29
|
nnzd |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. ZZ ) |
31 |
|
simpl3 |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> X e. B ) |
32 |
1 2
|
mulgcl |
|- ( ( G e. Grp /\ -u N e. ZZ /\ X e. B ) -> ( -u N .x. X ) e. B ) |
33 |
28 30 31 32
|
syl3anc |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u N .x. X ) e. B ) |
34 |
1 3
|
grpinvinv |
|- ( ( G e. Grp /\ ( -u N .x. X ) e. B ) -> ( I ` ( I ` ( -u N .x. X ) ) ) = ( -u N .x. X ) ) |
35 |
28 33 34
|
syl2anc |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( I ` ( I ` ( -u N .x. X ) ) ) = ( -u N .x. X ) ) |
36 |
1 2 3
|
mulgnegnn |
|- ( ( -u N e. NN /\ X e. B ) -> ( -u -u N .x. X ) = ( I ` ( -u N .x. X ) ) ) |
37 |
29 31 36
|
syl2anc |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u -u N .x. X ) = ( I ` ( -u N .x. X ) ) ) |
38 |
|
simprl |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> N e. RR ) |
39 |
38
|
recnd |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> N e. CC ) |
40 |
39
|
negnegd |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u -u N = N ) |
41 |
40
|
oveq1d |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u -u N .x. X ) = ( N .x. X ) ) |
42 |
37 41
|
eqtr3d |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( I ` ( -u N .x. X ) ) = ( N .x. X ) ) |
43 |
42
|
fveq2d |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( I ` ( I ` ( -u N .x. X ) ) ) = ( I ` ( N .x. X ) ) ) |
44 |
35 43
|
eqtr3d |
|- ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) ) |
45 |
|
simp2 |
|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> N e. ZZ ) |
46 |
|
elznn0nn |
|- ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) ) |
47 |
45 46
|
sylib |
|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) ) |
48 |
27 44 47
|
mpjaodan |
|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) ) |