Step |
Hyp |
Ref |
Expression |
1 |
|
lflnegcl.v |
|- V = ( Base ` W ) |
2 |
|
lflnegcl.r |
|- R = ( Scalar ` W ) |
3 |
|
lflnegcl.i |
|- I = ( invg ` R ) |
4 |
|
lflnegcl.n |
|- N = ( x e. V |-> ( I ` ( G ` x ) ) ) |
5 |
|
lflnegcl.f |
|- F = ( LFnl ` W ) |
6 |
|
lflnegcl.w |
|- ( ph -> W e. LMod ) |
7 |
|
lflnegcl.g |
|- ( ph -> G e. F ) |
8 |
2
|
lmodring |
|- ( W e. LMod -> R e. Ring ) |
9 |
6 8
|
syl |
|- ( ph -> R e. Ring ) |
10 |
|
ringgrp |
|- ( R e. Ring -> R e. Grp ) |
11 |
9 10
|
syl |
|- ( ph -> R e. Grp ) |
12 |
11
|
adantr |
|- ( ( ph /\ x e. V ) -> R e. Grp ) |
13 |
6
|
adantr |
|- ( ( ph /\ x e. V ) -> W e. LMod ) |
14 |
7
|
adantr |
|- ( ( ph /\ x e. V ) -> G e. F ) |
15 |
|
simpr |
|- ( ( ph /\ x e. V ) -> x e. V ) |
16 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
17 |
2 16 1 5
|
lflcl |
|- ( ( W e. LMod /\ G e. F /\ x e. V ) -> ( G ` x ) e. ( Base ` R ) ) |
18 |
13 14 15 17
|
syl3anc |
|- ( ( ph /\ x e. V ) -> ( G ` x ) e. ( Base ` R ) ) |
19 |
16 3
|
grpinvcl |
|- ( ( R e. Grp /\ ( G ` x ) e. ( Base ` R ) ) -> ( I ` ( G ` x ) ) e. ( Base ` R ) ) |
20 |
12 18 19
|
syl2anc |
|- ( ( ph /\ x e. V ) -> ( I ` ( G ` x ) ) e. ( Base ` R ) ) |
21 |
20 4
|
fmptd |
|- ( ph -> N : V --> ( Base ` R ) ) |
22 |
|
ringabl |
|- ( R e. Ring -> R e. Abel ) |
23 |
9 22
|
syl |
|- ( ph -> R e. Abel ) |
24 |
23
|
adantr |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> R e. Abel ) |
25 |
9
|
adantr |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> R e. Ring ) |
26 |
|
simpr1 |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> k e. ( Base ` R ) ) |
27 |
6
|
adantr |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> W e. LMod ) |
28 |
7
|
adantr |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> G e. F ) |
29 |
|
simpr2 |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> y e. V ) |
30 |
2 16 1 5
|
lflcl |
|- ( ( W e. LMod /\ G e. F /\ y e. V ) -> ( G ` y ) e. ( Base ` R ) ) |
31 |
27 28 29 30
|
syl3anc |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( G ` y ) e. ( Base ` R ) ) |
32 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
33 |
16 32
|
ringcl |
|- ( ( R e. Ring /\ k e. ( Base ` R ) /\ ( G ` y ) e. ( Base ` R ) ) -> ( k ( .r ` R ) ( G ` y ) ) e. ( Base ` R ) ) |
34 |
25 26 31 33
|
syl3anc |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( k ( .r ` R ) ( G ` y ) ) e. ( Base ` R ) ) |
35 |
|
simpr3 |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> z e. V ) |
36 |
2 16 1 5
|
lflcl |
|- ( ( W e. LMod /\ G e. F /\ z e. V ) -> ( G ` z ) e. ( Base ` R ) ) |
37 |
27 28 35 36
|
syl3anc |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( G ` z ) e. ( Base ` R ) ) |
38 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
39 |
16 38 3
|
ablinvadd |
|- ( ( R e. Abel /\ ( k ( .r ` R ) ( G ` y ) ) e. ( Base ` R ) /\ ( G ` z ) e. ( Base ` R ) ) -> ( I ` ( ( k ( .r ` R ) ( G ` y ) ) ( +g ` R ) ( G ` z ) ) ) = ( ( I ` ( k ( .r ` R ) ( G ` y ) ) ) ( +g ` R ) ( I ` ( G ` z ) ) ) ) |
40 |
24 34 37 39
|
syl3anc |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( I ` ( ( k ( .r ` R ) ( G ` y ) ) ( +g ` R ) ( G ` z ) ) ) = ( ( I ` ( k ( .r ` R ) ( G ` y ) ) ) ( +g ` R ) ( I ` ( G ` z ) ) ) ) |
41 |
|
eqid |
|- ( +g ` W ) = ( +g ` W ) |
42 |
|
eqid |
|- ( .s ` W ) = ( .s ` W ) |
43 |
1 41 2 42 16 38 32 5
|
lfli |
|- ( ( W e. LMod /\ G e. F /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( k ( .r ` R ) ( G ` y ) ) ( +g ` R ) ( G ` z ) ) ) |
44 |
27 28 26 29 35 43
|
syl113anc |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( k ( .r ` R ) ( G ` y ) ) ( +g ` R ) ( G ` z ) ) ) |
45 |
44
|
fveq2d |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( I ` ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) ) = ( I ` ( ( k ( .r ` R ) ( G ` y ) ) ( +g ` R ) ( G ` z ) ) ) ) |
46 |
16 32 3 25 26 31
|
ringmneg2 |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( k ( .r ` R ) ( I ` ( G ` y ) ) ) = ( I ` ( k ( .r ` R ) ( G ` y ) ) ) ) |
47 |
46
|
oveq1d |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( ( k ( .r ` R ) ( I ` ( G ` y ) ) ) ( +g ` R ) ( I ` ( G ` z ) ) ) = ( ( I ` ( k ( .r ` R ) ( G ` y ) ) ) ( +g ` R ) ( I ` ( G ` z ) ) ) ) |
48 |
40 45 47
|
3eqtr4d |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( I ` ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) ) = ( ( k ( .r ` R ) ( I ` ( G ` y ) ) ) ( +g ` R ) ( I ` ( G ` z ) ) ) ) |
49 |
1 2 42 16
|
lmodvscl |
|- ( ( W e. LMod /\ k e. ( Base ` R ) /\ y e. V ) -> ( k ( .s ` W ) y ) e. V ) |
50 |
27 26 29 49
|
syl3anc |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( k ( .s ` W ) y ) e. V ) |
51 |
1 41
|
lmodvacl |
|- ( ( W e. LMod /\ ( k ( .s ` W ) y ) e. V /\ z e. V ) -> ( ( k ( .s ` W ) y ) ( +g ` W ) z ) e. V ) |
52 |
27 50 35 51
|
syl3anc |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( ( k ( .s ` W ) y ) ( +g ` W ) z ) e. V ) |
53 |
|
2fveq3 |
|- ( x = ( ( k ( .s ` W ) y ) ( +g ` W ) z ) -> ( I ` ( G ` x ) ) = ( I ` ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) ) ) |
54 |
|
fvex |
|- ( I ` ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) ) e. _V |
55 |
53 4 54
|
fvmpt |
|- ( ( ( k ( .s ` W ) y ) ( +g ` W ) z ) e. V -> ( N ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( I ` ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) ) ) |
56 |
52 55
|
syl |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( N ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( I ` ( G ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) ) ) |
57 |
|
2fveq3 |
|- ( x = y -> ( I ` ( G ` x ) ) = ( I ` ( G ` y ) ) ) |
58 |
|
fvex |
|- ( I ` ( G ` y ) ) e. _V |
59 |
57 4 58
|
fvmpt |
|- ( y e. V -> ( N ` y ) = ( I ` ( G ` y ) ) ) |
60 |
29 59
|
syl |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( N ` y ) = ( I ` ( G ` y ) ) ) |
61 |
60
|
oveq2d |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( k ( .r ` R ) ( N ` y ) ) = ( k ( .r ` R ) ( I ` ( G ` y ) ) ) ) |
62 |
|
2fveq3 |
|- ( x = z -> ( I ` ( G ` x ) ) = ( I ` ( G ` z ) ) ) |
63 |
|
fvex |
|- ( I ` ( G ` z ) ) e. _V |
64 |
62 4 63
|
fvmpt |
|- ( z e. V -> ( N ` z ) = ( I ` ( G ` z ) ) ) |
65 |
35 64
|
syl |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( N ` z ) = ( I ` ( G ` z ) ) ) |
66 |
61 65
|
oveq12d |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( ( k ( .r ` R ) ( N ` y ) ) ( +g ` R ) ( N ` z ) ) = ( ( k ( .r ` R ) ( I ` ( G ` y ) ) ) ( +g ` R ) ( I ` ( G ` z ) ) ) ) |
67 |
48 56 66
|
3eqtr4d |
|- ( ( ph /\ ( k e. ( Base ` R ) /\ y e. V /\ z e. V ) ) -> ( N ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( k ( .r ` R ) ( N ` y ) ) ( +g ` R ) ( N ` z ) ) ) |
68 |
67
|
ralrimivvva |
|- ( ph -> A. k e. ( Base ` R ) A. y e. V A. z e. V ( N ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( k ( .r ` R ) ( N ` y ) ) ( +g ` R ) ( N ` z ) ) ) |
69 |
1 41 2 42 16 38 32 5
|
islfl |
|- ( W e. LMod -> ( N e. F <-> ( N : V --> ( Base ` R ) /\ A. k e. ( Base ` R ) A. y e. V A. z e. V ( N ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( k ( .r ` R ) ( N ` y ) ) ( +g ` R ) ( N ` z ) ) ) ) ) |
70 |
6 69
|
syl |
|- ( ph -> ( N e. F <-> ( N : V --> ( Base ` R ) /\ A. k e. ( Base ` R ) A. y e. V A. z e. V ( N ` ( ( k ( .s ` W ) y ) ( +g ` W ) z ) ) = ( ( k ( .r ` R ) ( N ` y ) ) ( +g ` R ) ( N ` z ) ) ) ) ) |
71 |
21 68 70
|
mpbir2and |
|- ( ph -> N e. F ) |