Step |
Hyp |
Ref |
Expression |
1 |
|
lfl0f.d |
|- D = ( Scalar ` W ) |
2 |
|
lfl0f.o |
|- .0. = ( 0g ` D ) |
3 |
|
lfl0f.v |
|- V = ( Base ` W ) |
4 |
|
lfl0f.f |
|- F = ( LFnl ` W ) |
5 |
2
|
fvexi |
|- .0. e. _V |
6 |
5
|
fconst |
|- ( V X. { .0. } ) : V --> { .0. } |
7 |
|
eqid |
|- ( Base ` D ) = ( Base ` D ) |
8 |
1 7 2
|
lmod0cl |
|- ( W e. LMod -> .0. e. ( Base ` D ) ) |
9 |
8
|
snssd |
|- ( W e. LMod -> { .0. } C_ ( Base ` D ) ) |
10 |
|
fss |
|- ( ( ( V X. { .0. } ) : V --> { .0. } /\ { .0. } C_ ( Base ` D ) ) -> ( V X. { .0. } ) : V --> ( Base ` D ) ) |
11 |
6 9 10
|
sylancr |
|- ( W e. LMod -> ( V X. { .0. } ) : V --> ( Base ` D ) ) |
12 |
1
|
lmodring |
|- ( W e. LMod -> D e. Ring ) |
13 |
12
|
ad2antrr |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> D e. Ring ) |
14 |
|
simplrl |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> r e. ( Base ` D ) ) |
15 |
|
eqid |
|- ( .r ` D ) = ( .r ` D ) |
16 |
7 15 2
|
ringrz |
|- ( ( D e. Ring /\ r e. ( Base ` D ) ) -> ( r ( .r ` D ) .0. ) = .0. ) |
17 |
13 14 16
|
syl2anc |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( r ( .r ` D ) .0. ) = .0. ) |
18 |
17
|
oveq1d |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( r ( .r ` D ) .0. ) ( +g ` D ) .0. ) = ( .0. ( +g ` D ) .0. ) ) |
19 |
|
ringgrp |
|- ( D e. Ring -> D e. Grp ) |
20 |
13 19
|
syl |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> D e. Grp ) |
21 |
7 2
|
grpidcl |
|- ( D e. Grp -> .0. e. ( Base ` D ) ) |
22 |
|
eqid |
|- ( +g ` D ) = ( +g ` D ) |
23 |
7 22 2
|
grplid |
|- ( ( D e. Grp /\ .0. e. ( Base ` D ) ) -> ( .0. ( +g ` D ) .0. ) = .0. ) |
24 |
20 21 23
|
syl2anc2 |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( .0. ( +g ` D ) .0. ) = .0. ) |
25 |
18 24
|
eqtrd |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( r ( .r ` D ) .0. ) ( +g ` D ) .0. ) = .0. ) |
26 |
|
simplrr |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> x e. V ) |
27 |
5
|
fvconst2 |
|- ( x e. V -> ( ( V X. { .0. } ) ` x ) = .0. ) |
28 |
26 27
|
syl |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( V X. { .0. } ) ` x ) = .0. ) |
29 |
28
|
oveq2d |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( r ( .r ` D ) ( ( V X. { .0. } ) ` x ) ) = ( r ( .r ` D ) .0. ) ) |
30 |
5
|
fvconst2 |
|- ( y e. V -> ( ( V X. { .0. } ) ` y ) = .0. ) |
31 |
30
|
adantl |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( V X. { .0. } ) ` y ) = .0. ) |
32 |
29 31
|
oveq12d |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( r ( .r ` D ) ( ( V X. { .0. } ) ` x ) ) ( +g ` D ) ( ( V X. { .0. } ) ` y ) ) = ( ( r ( .r ` D ) .0. ) ( +g ` D ) .0. ) ) |
33 |
|
simpll |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> W e. LMod ) |
34 |
|
eqid |
|- ( .s ` W ) = ( .s ` W ) |
35 |
3 1 34 7
|
lmodvscl |
|- ( ( W e. LMod /\ r e. ( Base ` D ) /\ x e. V ) -> ( r ( .s ` W ) x ) e. V ) |
36 |
33 14 26 35
|
syl3anc |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( r ( .s ` W ) x ) e. V ) |
37 |
|
simpr |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> y e. V ) |
38 |
|
eqid |
|- ( +g ` W ) = ( +g ` W ) |
39 |
3 38
|
lmodvacl |
|- ( ( W e. LMod /\ ( r ( .s ` W ) x ) e. V /\ y e. V ) -> ( ( r ( .s ` W ) x ) ( +g ` W ) y ) e. V ) |
40 |
33 36 37 39
|
syl3anc |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( r ( .s ` W ) x ) ( +g ` W ) y ) e. V ) |
41 |
5
|
fvconst2 |
|- ( ( ( r ( .s ` W ) x ) ( +g ` W ) y ) e. V -> ( ( V X. { .0. } ) ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = .0. ) |
42 |
40 41
|
syl |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( V X. { .0. } ) ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = .0. ) |
43 |
25 32 42
|
3eqtr4rd |
|- ( ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) /\ y e. V ) -> ( ( V X. { .0. } ) ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` D ) ( ( V X. { .0. } ) ` x ) ) ( +g ` D ) ( ( V X. { .0. } ) ` y ) ) ) |
44 |
43
|
ralrimiva |
|- ( ( W e. LMod /\ ( r e. ( Base ` D ) /\ x e. V ) ) -> A. y e. V ( ( V X. { .0. } ) ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` D ) ( ( V X. { .0. } ) ` x ) ) ( +g ` D ) ( ( V X. { .0. } ) ` y ) ) ) |
45 |
44
|
ralrimivva |
|- ( W e. LMod -> A. r e. ( Base ` D ) A. x e. V A. y e. V ( ( V X. { .0. } ) ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` D ) ( ( V X. { .0. } ) ` x ) ) ( +g ` D ) ( ( V X. { .0. } ) ` y ) ) ) |
46 |
3 38 1 34 7 22 15 4
|
islfl |
|- ( W e. LMod -> ( ( V X. { .0. } ) e. F <-> ( ( V X. { .0. } ) : V --> ( Base ` D ) /\ A. r e. ( Base ` D ) A. x e. V A. y e. V ( ( V X. { .0. } ) ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` D ) ( ( V X. { .0. } ) ` x ) ) ( +g ` D ) ( ( V X. { .0. } ) ` y ) ) ) ) ) |
47 |
11 45 46
|
mpbir2and |
|- ( W e. LMod -> ( V X. { .0. } ) e. F ) |