| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lfladd0l.v |
|- V = ( Base ` W ) |
| 2 |
|
lfladd0l.r |
|- R = ( Scalar ` W ) |
| 3 |
|
lfladd0l.p |
|- .+ = ( +g ` R ) |
| 4 |
|
lfladd0l.o |
|- .0. = ( 0g ` R ) |
| 5 |
|
lfladd0l.f |
|- F = ( LFnl ` W ) |
| 6 |
|
lfladd0l.w |
|- ( ph -> W e. LMod ) |
| 7 |
|
lfladd0l.g |
|- ( ph -> G e. F ) |
| 8 |
1
|
fvexi |
|- V e. _V |
| 9 |
8
|
a1i |
|- ( ph -> V e. _V ) |
| 10 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
| 11 |
2 10 1 5
|
lflf |
|- ( ( W e. LMod /\ G e. F ) -> G : V --> ( Base ` R ) ) |
| 12 |
6 7 11
|
syl2anc |
|- ( ph -> G : V --> ( Base ` R ) ) |
| 13 |
4
|
fvexi |
|- .0. e. _V |
| 14 |
13
|
a1i |
|- ( ph -> .0. e. _V ) |
| 15 |
2
|
lmodring |
|- ( W e. LMod -> R e. Ring ) |
| 16 |
|
ringgrp |
|- ( R e. Ring -> R e. Grp ) |
| 17 |
6 15 16
|
3syl |
|- ( ph -> R e. Grp ) |
| 18 |
10 3 4
|
grplid |
|- ( ( R e. Grp /\ k e. ( Base ` R ) ) -> ( .0. .+ k ) = k ) |
| 19 |
17 18
|
sylan |
|- ( ( ph /\ k e. ( Base ` R ) ) -> ( .0. .+ k ) = k ) |
| 20 |
9 12 14 19
|
caofid0l |
|- ( ph -> ( ( V X. { .0. } ) oF .+ G ) = G ) |