Step |
Hyp |
Ref |
Expression |
1 |
|
lfldi.v |
|- V = ( Base ` W ) |
2 |
|
lfldi.r |
|- R = ( Scalar ` W ) |
3 |
|
lfldi.k |
|- K = ( Base ` R ) |
4 |
|
lfldi.p |
|- .+ = ( +g ` R ) |
5 |
|
lfldi.t |
|- .x. = ( .r ` R ) |
6 |
|
lfldi.f |
|- F = ( LFnl ` W ) |
7 |
|
lfldi.w |
|- ( ph -> W e. LMod ) |
8 |
|
lfldi.x |
|- ( ph -> X e. K ) |
9 |
|
lfldi2.y |
|- ( ph -> Y e. K ) |
10 |
|
lfldi2.g |
|- ( ph -> G e. F ) |
11 |
1
|
fvexi |
|- V e. _V |
12 |
11
|
a1i |
|- ( ph -> V e. _V ) |
13 |
2 3 1 6
|
lflf |
|- ( ( W e. LMod /\ G e. F ) -> G : V --> K ) |
14 |
7 10 13
|
syl2anc |
|- ( ph -> G : V --> K ) |
15 |
|
fconst6g |
|- ( X e. K -> ( V X. { X } ) : V --> K ) |
16 |
8 15
|
syl |
|- ( ph -> ( V X. { X } ) : V --> K ) |
17 |
|
fconst6g |
|- ( Y e. K -> ( V X. { Y } ) : V --> K ) |
18 |
9 17
|
syl |
|- ( ph -> ( V X. { Y } ) : V --> K ) |
19 |
2
|
lmodring |
|- ( W e. LMod -> R e. Ring ) |
20 |
7 19
|
syl |
|- ( ph -> R e. Ring ) |
21 |
3 4 5
|
ringdi |
|- ( ( R e. Ring /\ ( x e. K /\ y e. K /\ z e. K ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) ) |
22 |
20 21
|
sylan |
|- ( ( ph /\ ( x e. K /\ y e. K /\ z e. K ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) ) |
23 |
12 14 16 18 22
|
caofdi |
|- ( ph -> ( G oF .x. ( ( V X. { X } ) oF .+ ( V X. { Y } ) ) ) = ( ( G oF .x. ( V X. { X } ) ) oF .+ ( G oF .x. ( V X. { Y } ) ) ) ) |